Encyclopedia Gravity Gravity Analysis Spectral Convergence

ARTICLE 4 claims 4 theorems

Gravity Analysis Spectral Convergence

A toolkit of proved theorems shows how discrete approximations to curved space converge to their continuous limits, with explicit error rates.

Verify this page

Spectral convergence

Spectral convergence is the study of how the eigenvalues of a discrete system, such as a lattice of points, approach the eigenvalues of a continuous system as the lattice gets finer. In Recognition Science, this appears when a curved space is approximated by a discrete grid. The central question is whether the discrete eigenvalues, which describe the allowed frequencies of vibration on the grid, settle down to the eigenvalues of the continuous curved space as the grid spacing shrinks to zero.

The classical starting point is the flat case. On a circle of circumference 2π, the allowed frequencies are the integers and their squares. On a discrete lattice with N points, the frequencies are given by 4N² sin²(πk/N), where k is the wavenumber. A theorem in the machine-checked library proves that this discrete expression converges to (2πk)², the continuous result, as N grows. More importantly, the theorem provides an explicit rate: the error is at most ((2πk)⁴/12)/N². This means the approximation improves quadratically as the lattice resolution increases, a sharp quantitative bound that a later phase of the campaign will use for curved spaces.

The proof of this rate relies on a global bound on the sine function. The standard library bound only holds for small arguments, but here the argument πk/N is not small for large wavenumbers. The toolkit proves that |sin t - t| ≤ t³/6 for all t ≥ 0, without any smallness condition. This is a simple consequence of the Taylor expansion and monotonicity, but it is exactly what the eigenvalue expansion needs.

Two further theorems complete the toolkit. The first, spectral gap persistence, states that if two eigenvalue branches converge to distinct limits, they eventually separate. This is the tool used to keep curved eigenvalue branches apart. The second is a general squeeze theorem: if a sequence of eigenvalues is bounded by C/N², then it converges. Together, these results form a reusable analysis package for the campaign's Phase 4, which applies curved operator convergence branch by branch.

In Recognition Science, this toolkit is a step toward showing that the discrete recognition ledger, a finite record of events, can approximate the continuous geometry it describes. The theorems prove that the approximation is not just qualitative but quantitative, with explicit error bounds that shrink quadratically. This is a necessary ingredient for the framework's claim that its discrete foundations recover continuous physics.

THEOREM discrete_sine_eigenvalue_tendsto · IndisputableMonolith/Gravity/Analysis/SpectralConvergence.lean
discrete_sine_eigenvalue_tendsto · IndisputableMonolith/Gravity/Analysis/SpectralConvergence.lean:164 
/-- THEOREM (rated limit, composing the toolkit). The flat discrete TT
eigenvalue `4N² sin²(πk/N)` converges to `(2πk)²`, obtained by feeding the
quantitative expansion into `eigenvalue_limit_of_uniform_bound` with
`C = (2πk)⁴/12`. Re-derives
`DiscreteLichnerowicz.discreteEigenvalue_tendsto` with an explicit rate. -/
theorem discrete_sine_eigenvalue_tendsto (k : ℕ) :
    Filter.Tendsto
      (fun N : ℕ => 4 * (N : ℝ) ^ 2 * Real.sin (Real.pi * (k : ℝ) / (N : ℝ)) ^ 2)
      Filter.atTop (nhds ((2 * Real.pi * (k : ℝ)) ^ 2)) :=
  eigenvalue_limit_of_uniform_bound _ _ ((2 * Real.pi * (k : ℝ)) ^ 4 / 12) 1
    (fun N hN => discrete_sine_eigenvalue_expansion k N hN)
THEOREM discrete_sine_eigenvalue_expansion · IndisputableMonolith/Gravity/Analysis/SpectralConvergence.lean
discrete_sine_eigenvalue_expansion · IndisputableMonolith/Gravity/Analysis/SpectralConvergence.lean:115 
/-- 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 abs_sin_sub_le_cube · IndisputableMonolith/Gravity/Analysis/SpectralConvergence.lean
abs_sin_sub_le_cube · IndisputableMonolith/Gravity/Analysis/SpectralConvergence.lean:103 
/-- THEOREM (global cubic Taylor bound for sine). For `t ≥ 0`,
`|sin t - t| ≤ t³/6`. Combines `Real.sin_le` (upper) with
`sub_cube_le_sin` (lower). Unlike Mathlib's `Real.sin_bound`, no `|t| ≤ 1`
hypothesis is needed. -/
theorem abs_sin_sub_le_cube (t : ℝ) (ht : 0 ≤ t) :
    |Real.sin t - t| ≤ t ^ 3 / 6 := by
  have h1 : Real.sin t ≤ t := Real.sin_le ht
  have h2 : t - t ^ 3 / 6 ≤ Real.sin t := sub_cube_le_sin t ht
  have h3 : 0 ≤ t ^ 3 / 6 := by positivity
  rw [abs_le]
  constructor <;> linarith
THEOREM spectrum_gap_persistence · IndisputableMonolith/Gravity/Analysis/SpectralConvergence.lean
spectrum_gap_persistence · IndisputableMonolith/Gravity/Analysis/SpectralConvergence.lean:176 
/-- 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 toolkit does not prove convergence for curved spaces, only for the flat case. It does not establish the physical recognition-to-linking bridge for gravity. It does not derive the value of any physical constant. It does not claim the min-max perturbation theorem, which is recorded as future work.

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:

MACHINE LAYER · GROUNDED CLAIM TABLE · CLICK TO EXPAND