Gravity Analysis Spectral Convergence Const Div Sq Tendsto Zero

A limit that keeps its distance

In analysis, one of the most useful facts is also one of the simplest: if you divide a fixed number by an ever-larger square, the result gets arbitrarily close to zero. For example, 100 divided by 1, then by 4, then by 9, then by 16, produces 100, 25, 11.1, 6.25, and the sequence keeps falling toward zero. The theorem const_div_sq_tendsto_zero is the formal, machine-checked version of this observation. It states that for any real constant C, the expression C divided by N squared tends to zero as the natural number N grows without bound.

The proof is a short exercise in limits. The square of N itself tends to infinity, and a constant divided by something that grows without bound tends to zero. The declaration records this in the language of filters: the function sending N to C over N squared has the filter atTop mapped to the neighborhood of zero. This is not a new physical law or a deep discovery; it is a foundational tool, the kind of lemma that appears silently inside larger arguments.

Its purpose in the framework's library is to serve as the backbone of a squeeze argument. A separate theorem, eigenvalue_limit_of_uniform_bound, uses it to show that if a sequence of numbers is trapped within a distance C over N squared of some target value, then that sequence must converge to the target. This is the rated version of convergence: not just that something converges, but that it does so with a known speed, bounded by a constant divided by N squared.

That rated convergence matters when a discrete grid with N points is used to approximate a continuous system. The theorem discrete_sine_eigenvalue_expansion applies this to the eigenvalues of a discrete sine operator, showing that the error between the discrete and continuous eigenvalues is at most a constant times (2πk)⁴ divided by 12 N². The qualitative fact that these eigenvalues converge was already known; this toolkit upgrades it to a quantitative statement with an explicit error bound. The final theorem, discrete_sine_eigenvalue_tendsto, re-derives the qualitative limit from this rate, confirming that the pieces fit together.

In Recognition Science, this toolkit is preparation for a later phase that will handle curved spaces. The claim is narrow: it establishes a rate of convergence for a flat, discrete model. It does not prove anything about curved geometry, gravity, or the physical universe. It does not even assert that the discrete model is physically correct. It only guarantees that, in this flat model, the discrete eigenvalues approach the continuous ones at a known speed, and that this speed is enough to keep spectral gaps from collapsing.

The value of this result is that it turns a vague promise of approximation into a precise contract. When a later argument needs to know how fast a discrete model converges to its continuous limit, this theorem provides the answer: the error shrinks like a constant over N squared. That is the kind of guarantee that lets a larger proof proceed without hand-waving.

/-- Helper: `C / N² → 0` as `N → ∞` over the naturals. -/
theorem const_div_sq_tendsto_zero (C : ℝ) :
    Filter.Tendsto (fun N : ℕ => C / (N : ℝ) ^ 2) Filter.atTop (nhds 0) := by
  have hpow : Filter.Tendsto (fun N : ℕ => ((N : ℝ)) ^ 2) Filter.atTop Filter.atTop := by
    have h1 : Filter.Tendsto (fun x : ℝ => x ^ 2) Filter.atTop Filter.atTop :=
      tendsto_pow_atTop two_ne_zero
    exact h1.comp tendsto_natCast_atTop_atTop
  exact tendsto_const_nhds.div_atTop hpow

/-- 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

What this page does not claim

This theorem says nothing about curved geometry or physical gravity. It does not assert that the discrete sine model is physically correct. It does not prove that the error constant (2πk)⁴/12 is optimal.

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: