Encyclopedia Gravity Gravity Analysis Spectral Convergence Discrete Sine Eigenvalue Expansion

ARTICLE 3 claims 3 theorems

Gravity Analysis Spectral Convergence Discrete Sine Eigenvalue Expansion

A proved bound that tells you how fast a discrete approximation to a vibrating system approaches the true continuous one.

Verify this page

The discrete sine expansion

When a physicist or engineer studies a vibrating string, a drumhead, or a gravitational wave, they often replace a continuous system with a discrete grid of points. The discrete sine eigenvalue expansion is a theorem about how well that replacement works. It gives a precise, proved bound on the difference between the discrete system's allowed vibration frequencies and the true continuous ones. The bound says the error shrinks like one over the square of the number of grid points, which is a fast and predictable rate of convergence.

The theorem itself is a quantitative statement about the eigenvalues of a discrete sine transform. For a grid with N points and a wavenumber k, the discrete eigenvalue is 4N² sin²(πk/N), while the continuous eigenvalue is (2πk)². The theorem proves that the absolute difference between these two is at most ((2πk)⁴/12) / N². This is a sharp, explicit bound that holds for every wavenumber and every grid resolution, with no smallness assumption on the wavenumber. The proof relies on a global cubic Taylor bound for the sine function, which is also proved in the same file.

This result upgrades an earlier qualitative statement, which merely said the discrete eigenvalues converge to the continuous ones, into a quantitative one with a specific rate. It is a piece of a larger toolkit for spectral convergence, which includes a lemma that turns such a bound into a limit, and another that shows spectral gaps persist under discretization. The toolkit is designed for a campaign that studies curved operators, where such explicit rates are needed for perturbation arguments.

In Recognition Science, this theorem is part of the framework's machine-checked library of formal theorems. The framework models physical structure from a ledger of recognition events, and this expansion is a technical tool within that project. The theorem is proved in the Lean proof assistant, with no unproved axioms beyond the standard ones. It is a statement about a specific mathematical object, not a physical claim about the universe.

What the theorem does not claim is just as important. It does not say that the discrete approximation is always accurate for any physical problem; it only bounds the error in the eigenvalues for this specific sine transform. It does not prove anything about curved spaces or general relativity, despite being part of a campaign that aims to study them. It is a foundational, reusable result, not a complete theory of anything.

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

What this page does not claim

The theorem does not apply to curved spaces or general relativity, despite being part of a campaign that aims to study them. It does not say the discrete approximation is always accurate for any physical problem. It does not prove the min-max perturbation lemma, which remains 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