Gravity Analysis Spectral Convergence Eigenvalue Limit Of Uniform Bound

The squeeze theorem

Recognition Science, a framework that derives physical structure from a discrete record of events, often works with approximations that improve as a resolution parameter N grows. A recurring question is whether a sequence of approximate values actually converges to a true value. The declaration eigenvalue_limit_of_uniform_bound answers this with a clean squeeze: if the error between each approximate value and the target is bounded by a constant divided by N squared, then the approximations must converge to the target. In symbols, if |λ_N − Λ| ≤ C/N² for all large N, then λ_N → Λ. The proof is short: the bound C/N² itself shrinks to zero as N grows, so the error is squeezed between zero and something that vanishes.

This is a standard tool in numerical analysis, and the framework's library of machine-checked formal theorems records it as a proved result. The declaration is not a claim about gravity itself. It is a general lemma about sequences of real numbers. Its role is to name a pattern that later phases of the framework's gravity analysis apply to specific eigenvalue branches, which are the discrete energy levels of a system. The power of the lemma is that it turns a quantitative rate of convergence into a qualitative statement of convergence, and it does so once, so the later work can cite it instead of re-proving the same squeeze argument each time.

The framework pairs this lemma with a sharper, quantitative result for a specific discrete operator. For a sine-based eigenvalue formula, the library proves that the error is bounded by a constant times (2πk)⁴/12 divided by N², where k is a wavenumber. Feeding this explicit bound into the general squeeze lemma re-derives the known qualitative limit with an explicit rate. The library also proves that if two eigenvalue branches converge to different limits, they eventually separate, a property that keeps curved branches distinct in later analysis. These are all theorems in the machine-checked library, meaning they are proved from the standard axioms of the underlying logic with no unproved assumptions.

What the declaration does not claim is just as important. It does not assert that any particular physical system has eigenvalues satisfying the bound; that is a separate, domain-specific question. It does not establish the value of any limit Λ; the lemma takes Λ as an input. And it does not prove the min-max characterization of eigenvalues, which the campaign brief lists as future work. The lemma is a bridge, not a destination: it says how to get from a rate to a limit, and it leaves the physics of the rate to the theorems that supply it.

For a reader, the practical takeaway is that the framework has a reusable, verified tool for one of the most common moves in spectral analysis. When a later phase needs to show that discrete approximations settle down to a continuum limit, it can invoke this squeeze lemma with confidence, because the proof is already checked. The lemma is a small but load-bearing piece of the framework's gravity analysis, and its value lies in being exactly as general as it claims to be.

/-- THEOREM (squeeze with rate). If the discrete eigenvalues `lam N` satisfy
`|lam N - Λ| ≤ C/N²` for all `N ≥ N₀`, then `lam N → Λ`. Trivial, but it
names the pattern Phase 4 applies to every curved eigenvalue branch. -/
theorem eigenvalue_limit_of_uniform_bound (lam : ℕ → ℝ) (Λ C : ℝ) (N₀ : ℕ)
    (h : ∀ N : ℕ, N₀ ≤ N → |lam N - Λ| ≤ C / (N : ℝ) ^ 2) :
    Filter.Tendsto lam Filter.atTop (nhds Λ) := by
  rw [tendsto_iff_dist_tendsto_zero]
  refine squeeze_zero' (Filter.Eventually.of_forall fun N => dist_nonneg) ?_
    (const_div_sq_tendsto_zero C)
  filter_upwards [Filter.eventually_ge_atTop N₀] with N hN
  rw [Real.dist_eq]
  exact h N hN

/-- THEOREM (quantitative flat TT eigenvalue expansion). For every
wavenumber `k` and lattice resolution `N ≥ 1`,

`|4N² sin²(πk/N) - (2πk)²| ≤ ((2πk)⁴/12) / N²`.

This is the sharp rate behind the qualitative limit
`DiscreteLichnerowicz.discreteEigenvalue_tendsto`. Derivation: with
`x = πk/N` we have `(2πk)² = 4N²x²`, so the error factors as
`4N² (sin x - x)(sin x + x)`; then `|sin x - x| ≤ x³/6`
(`abs_sin_sub_le_cube`) and `|sin x + x| ≤ 2x` give the bound
`(4/3) N² x⁴ = ((2πk)⁴/12)/N²`. Phase 4 curved perturbation bounds consume
this explicit constant `C(k) = (2πk)⁴/12`. -/
theorem discrete_sine_eigenvalue_expansion (k N : ℕ) (hN : 1 ≤ N) :
    |4 * (N : ℝ) ^ 2 * Real.sin (Real.pi * (k : ℝ) / (N : ℝ)) ^ 2
        - (2 * Real.pi * (k : ℝ)) ^ 2|
      ≤ (2 * Real.pi * (k : ℝ)) ^ 4 / 12 / (N : ℝ) ^ 2 := by
  have hNpos : (0 : ℝ) < (N : ℝ) := by exact_mod_cast hN
  have hN0 : (N : ℝ) ≠ 0 := ne_of_gt hNpos
  set x : ℝ := Real.pi * (k : ℝ) / (N : ℝ) with hxdef
  have hx0 : 0 ≤ x := by
    rw [hxdef]
    exact div_nonneg (mul_nonneg Real.pi_pos.le (Nat.cast_nonneg k)) hNpos.le
  have hkey : (2 * Real.pi * (k : ℝ)) ^ 2 = 4 * (N : ℝ) ^ 2 * x ^ 2 := by
    rw [hxdef]
    field_simp
    ring
  have hfac : 4 * (N : ℝ) ^ 2 * Real.sin x ^ 2 - (2 * Real.pi * (k : ℝ)) ^ 2
      = (4 * (N : ℝ) ^ 2) * ((Real.sin x - x) * (Real.sin x + x)) := by
    rw [hkey]
    ring
  have h4N : |4 * (N : ℝ) ^ 2| = 4 * (N : ℝ) ^ 2 := abs_of_nonneg (by positivity)
  have hbound1 : |Real.sin x - x| ≤ x ^ 3 / 6 := abs_sin_sub_le_cube x hx0
  have hbound2 : |Real.sin x + x| ≤ 2 * x := by
    calc |Real.sin x + x| ≤ |Real.sin x| + |x| := abs_add_le _ _
      _ ≤ |x| + |x| := by
          have := Real.abs_sin_le_abs (x := x)
          linarith
      _ = 2 * x := by rw [abs_of_nonneg hx0]; ring
  calc |4 * (N : ℝ) ^ 2 * Real.sin x ^ 2 - (2 * Real.pi * (k : ℝ)) ^ 2|
      = (4 * (N : ℝ) ^ 2) * (|Real.sin x - x| * |Real.sin x + x|) := by
        rw [hfac, abs_mul, h4N, abs_mul]
    _ ≤ (4 * (N : ℝ) ^ 2) * (x ^ 3 / 6 * (2 * x)) := by
        refine mul_le_mul_of_nonneg_left ?_ (by positivity)
        exact mul_le_mul hbound1 hbound2 (abs_nonneg _) (by positivity)
    _ = (2 * Real.pi * (k : ℝ)) ^ 4 / 12 / (N : ℝ) ^ 2 := by
        rw [hxdef]
        field_simp
        ring

/-- THEOREM (gap persistence). If two eigenvalue branches converge to
distinct limits `Λ < Μ`, then eventually `lam N < mu N`: spectral gaps
survive discretization for large `N`. The tool Phase 4 uses to separate
curved eigenvalue branches. -/
theorem spectrum_gap_persistence (lam mu : ℕ → ℝ) (Λ Μ : ℝ)
    (hlam : Filter.Tendsto lam Filter.atTop (nhds Λ))
    (hmu : Filter.Tendsto mu Filter.atTop (nhds Μ))
    (hlt : Λ < Μ) :
    ∀ᶠ N : ℕ in Filter.atTop, lam N < mu N :=
  hlam.eventually_lt hmu hlt

What this page does not claim

The lemma does not assert that any particular physical system satisfies the C/N² bound. The lemma does not establish the value of any limit Λ. The lemma does not prove the min-max characterization of eigenvalues.

Verify this page

Every tagged claim above names its theorem. To check one yourself rather than trust this page, elaborate the source module with Lean 4 and audit its axiom basis:

$ lake env lean IndisputableMonolith/Gravity/Analysis/SpectralConvergence.lean
expected axiom basis: [propext, Classical.choice, Quot.sound] (the Lean kernel's standard three; no RS-specific axioms)

A page whose claims cannot be reproduced this way does not ship. In production, every anchor links to the exact declaration in the public source release, and this block carries the build receipt for the page itself.

Derived articles

This page is generated by a question-recursion engine: the questions its answers raise become the next pages. The current agenda, with open targets marked red: