Gravity Analysis Spectral Convergence Discrete Sine Eigenvalue Tendsto

The discrete sine eigenvalue limit

The discrete sine eigenvalue is a number that comes from a simple model of a vibrating string. A string of length 1, divided into N equal segments. The possible vibration frequencies of this segmented string are given by the formula 4N² sin²(πk/N), where k is a positive whole number called the wavenumber, labeling which harmonic you are looking at. As N grows, this discrete model should resemble the continuous string, whose frequencies are (2πk)². The declaration discrete_sine_eigenvalue_tendsto is a formal theorem stating that, for any fixed wavenumber k, the discrete frequency 4N² sin²(πk/N) converges to the continuous frequency (2πk)² as the number of segments N tends to infinity.

The proof does not just show convergence; it shows how fast. A companion theorem, discrete_sine_eigenvalue_expansion, proves a sharp error bound: the difference between the discrete and continuous frequencies is at most ((2πk)⁴/12)/N². This means that doubling the resolution N makes the error four times smaller. The convergence theorem is derived by feeding this explicit error rate into a general squeeze lemma, eigenvalue_limit_of_uniform_bound, which states that if a sequence is eventually within C/N² of a limit, it converges to that limit. This composition is itself checked by the machine, so the whole chain is a single airtight result.

The result is part of a larger toolkit in the machine-checked library of formal theorems, built to support a campaign on gravity. The toolkit's purpose is to provide reusable analysis tools for a later phase that will handle curved spaces. The explicit error rate here is what that later phase needs: when a space is not perfectly flat, the discrete frequencies are expected to be close to these flat-space values, and the rate tells you how close. The theorem also verifies that the toolkit's two main pieces, the error bound and the squeeze lemma, work together correctly.

In Recognition Science, this theorem is a step toward understanding how discrete models of spacetime approach continuous ones. The framework models physical structure as a discrete ledger of recognition events, and this result shows that a discrete approximation of a vibrating system converges to the continuous ideal in a controlled way. It is a mathematical fact about a specific formula, not a physical claim about gravity itself. The theorem does not say anything about whether the discrete model is the correct description of reality; it only says that if you use this particular discrete model, its frequencies approach the continuous ones at a known rate.

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

What this page does not claim

This theorem does not claim that the discrete model is physically correct for gravity. It does not prove convergence for curved spaces, only for the flat discrete sine model. It does not claim a specific rate for eigenvalue gaps, only for the individual 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: