Encyclopedia Gravity Gravity Seven Gaps Discrete Lichnerowicz Discrete Tt Spectrum Converges To Flat

ARTICLE 4 claims 3 theorems 1 open

Gravity Seven Gaps Discrete Lichnerowicz Discrete Tt Spectrum Converges To Flat

On a flat three-torus, the vibration frequencies of a lattice of points approach the continuous gravitational-wave frequencies as the lattice gets finer, in one direction only.

Verify this page

The discrete spectrum

The Lichnerowicz operator is the mathematical engine of gravitational waves: it is the operator whose vibration modes, on a curved spacetime, describe how ripples in the geometry propagate. On a flat background, its action on transverse-traceless tensors reduces to the ordinary Laplacian. The declaration discrete_tt_spectrum_converges_to_flat_lichnerowicz is a machine-checked theorem that connects a discrete, lattice-based approximation of this operator to its continuous counterpart on a flat three-torus.

The setup is concrete. A three-torus is a cube with opposite faces identified, a finite volume with no boundary. The discrete model places a grid of points on this torus, with spacing h = 1/N, and defines a discrete Laplacian on the grid. The theorem proves that for a fixed wavenumber k, the discrete eigenvalue of the axis-aligned plane wave, 4N²sin²(πk/N), converges to (2πk)² as the grid is refined, N → ∞. The value (2πk)² is the genuine eigenvalue of the continuous Laplacian on the same axis-aligned wave. The proof also establishes that the two standard gravitational-wave polarizations, plus and cross, are symmetric, traceless, and linearly independent, and that the axis plane wave is exactly transverse under the discrete divergence.

This is a sector result, not a full recovery. The convergence is proved only for plane waves traveling along a single axis, k = (k, 0, 0), acted on by a componentwise axis stencil. A separate test in the library showed that the continuum moment tensor of the canonical frozen energy is anisotropic: the body-diagonal direction is roughly 4.9 times stiffer than an axis direction. Axis stencils are blind to that anisotropy, so the theorem must not be read as isotropic flat-space recovery of the full Lichnerowicz spectrum. The direction-resolved symbol question remains open.

What the theorem does not claim is as important as what it proves. It does not treat curved backgrounds: Schwarzschild, Kerr, or any quasinormal-mode spectra are explicitly open. The flat-background reduction of the Lichnerowicz operator to the Laplacian is encoded as a definition, not a curved-space theorem. The theorem is a precise, narrow bridge: it shows that on a flat three-torus, along one axis, the discrete spectrum converges to the continuous one.

THEOREM discreteEigenvalue_tendsto · IndisputableMonolith/Gravity/SevenGaps/DiscreteLichnerowicz.lean
discreteEigenvalue_tendsto · IndisputableMonolith/Gravity/SevenGaps/DiscreteLichnerowicz.lean:204 
/-- THEOREM (the core convergence result; AXIS SECTOR ONLY). For fixed
wavenumber `k`, the discrete eigenvalue `4 N² sin²(πk/N)` of the AXIS mode
converges to the continuum eigenvalue `(2πk)²` as the lattice is refined.
Proof: `4N² sin²(πk/N) = (2πk)² (sin x / x)²` with `x = πk/N → 0`, and
`sin x / x → 1` at `0` (from `HasDerivAt sin 1 0` via the slope
characterization); the wavenumber `k = 0` is handled separately (both sides
vanish identically).

Scope: this is a statement about axis-aligned modes of the axis-stencil
Laplacian. Test G (`FreudenthalStencilPreflight`/`FreudenthalEnergyLimit`,
commits 7b808f75b4, 1d3ed6da06) kernel-proved the full continuum moment
tensor is anisotropic, `A₀ = (1+√2)I + (√2+√3)J`, which axis stencils
cannot see; do not read this as isotropic flat-space recovery. The
direction-resolved symbol question is governed by the C10 probe (plan
receipt P-iso, 2026-07-15). -/
theorem discreteEigenvalue_tendsto (k : ℕ) :
    Filter.Tendsto (fun N : ℕ => discreteEigenvalue N k) Filter.atTop
      (nhds ((2 * Real.pi * (k : ℝ)) ^ 2)) := by
  rcases Nat.eq_zero_or_pos k with hk | hk
  · subst hk
    have hzero : (fun N : ℕ => discreteEigenvalue N 0) = fun _ : ℕ => (0 : ℝ) := by
      funext N
      norm_num [discreteEigenvalue]
    rw [hzero]
    have h0 : ((2 * Real.pi * ((0 : ℕ) : ℝ)) ^ 2 : ℝ) = 0 := by norm_num
    rw [h0]
    exact tendsto_const_nhds
  · have hk' : (0 : ℝ) < (k : ℝ) := by exact_mod_cast hk
    -- sin y / y → 1 as y → 0 (through nonzero values)
    have hslope : Filter.Tendsto (fun y : ℝ => Real.sin y / y) (𝓝[≠] (0 : ℝ)) (nhds 1) := by
      have h := Real.hasDerivAt_sin 0
      rw [Real.cos_zero] at h
      have h2 := hasDerivAt_iff_tendsto_slope.mp h
      refine h2.congr ?_
      intro y
      rw [slope_def_field]
      simp
    -- x_N = πk/N → 0 within nonzero values
    have hx0 : Filter.Tendsto (fun N : ℕ => Real.pi * (k : ℝ) / (N : ℝ)) Filter.atTop
        (nhds 0) := tendsto_const_div_atTop_nhds_zero_nat (Real.pi * (k : ℝ))
    have hxmem : ∀ᶠ N : ℕ in Filter.atTop,
        Real.pi * (k : ℝ) / (N : ℝ) ∈ ({0}ᶜ : Set ℝ) := by
      filter_upwards [Filter.eventually_ge_atTop 1] with N hN
      have hNpos : (0 : ℝ) < (N : ℝ) := by exact_mod_cast hN
      have hpos : 0 < Real.pi * (k : ℝ) / (N : ℝ) :=
        div_pos (mul_pos Real.pi_pos hk') hNpos
      simp only [Set.mem_compl_iff, Set.mem_singleton_iff]
      exact ne_of_gt hpos
    have hx : Filter.Tendsto (fun N : ℕ => Real.pi * (k : ℝ) / (N : ℝ)) Filter.atTop
        (𝓝[≠] (0 : ℝ)) :=
      tendsto_nhdsWithin_of_tendsto_nhds_of_eventually_within _ hx0 hxmem
    have hcomp := hslope.comp hx
    simp only [Function.comp_def] at hcomp
    have hmul : Filter.Tendsto
        (fun N : ℕ => (2 * Real.pi * (k : ℝ)) ^ 2
          * (Real.sin (Real.pi * (k : ℝ) / (N : ℝ)) / (Real.pi * (k : ℝ) / (N : ℝ))) ^ 2)
        Filter.atTop (nhds ((2 * Real.pi * (k : ℝ)) ^ 2 * 1 ^ 2)) :=
      tendsto_const_nhds.mul (hcomp.pow 2)
    rw [one_pow, mul_one] at hmul
    refine hmul.congr' ?_
    filter_upwards [Filter.eventually_ge_atTop 1] with N hN
    have hNpos : (0 : ℝ) < (N : ℝ) := by exact_mod_cast hN
    have hN0 : (N : ℝ) ≠ 0 := ne_of_gt hNpos
    have hπk : Real.pi * (k : ℝ) ≠ 0 := ne_of_gt (mul_pos Real.pi_pos hk')
    simp only [discreteEigenvalue]
    field_simp
    ring
THEOREM polarizations_linearIndependent · IndisputableMonolith/Gravity/SevenGaps/DiscreteLichnerowicz.lean
polarizations_linearIndependent · IndisputableMonolith/Gravity/SevenGaps/DiscreteLichnerowicz.lean:408 
/-- THEOREM. The two standard polarizations are linearly independent over ℂ:
they span the 2D TT polarization space for the axis wave. -/
theorem polarizations_linearIndependent :
    LinearIndependent ℂ ![epsPlus, epsCross] := by
  rw [linearIndependent_fin2]
  constructor
  · intro h
    have h12 : (![epsPlus, epsCross] 1) 1 2 = (0 : Matrix (Fin 3) (Fin 3) ℂ) 1 2 := by
      rw [h]
    have e1 : (![epsPlus, epsCross] 1) 1 2 = (1 : ℂ) := rfl
    have e2 : ((0 : Matrix (Fin 3) (Fin 3) ℂ) 1 2 : ℂ) = 0 := rfl
    rw [e1, e2] at h12
    exact one_ne_zero h12
  · intro a h
    have h11 : (a • ![epsPlus, epsCross] 1) 1 1 = (![epsPlus, epsCross] 0) 1 1 := by
      rw [h]
    have e1 : (a • ![epsPlus, epsCross] 1) 1 1 = a * 0 := rfl
    have e2 : ((![epsPlus, epsCross] 0) 1 1 : ℂ) = 1 := rfl
    rw [e1, e2, mul_zero] at h11
    exact zero_ne_one h11
THEOREM planeH · IndisputableMonolith/Gravity/SevenGaps/DiscreteLichnerowicz.lean
planeH · IndisputableMonolith/Gravity/SevenGaps/DiscreteLichnerowicz.lean:312 
/-- Axis plane wave `k = (k, 0, 0)`: the 1D Fourier mode in the first
coordinate times a constant polarization matrix. -/
noncomputable def planeH (N : ℕ) (k : ℤ) (eps : Matrix (Fin 3) (Fin 3) ℂ) :
    LatticeTensorField :=
  fun x => fourierMode N k x.1 • eps
OPEN status_curved_background_open · IndisputableMonolith/Gravity/SevenGaps/DiscreteLichnerowicz.lean
status_curved_background_open · IndisputableMonolith/Gravity/SevenGaps/DiscreteLichnerowicz.lean:565 
theorem status_curved_background_open :
    status.curved_background_open = true := rfl

What this page does not claim

The theorem does not claim isotropic flat-space recovery of the full Lichnerowicz spectrum. It does not claim any result on curved backgrounds or quasinormal-mode spectra. The flat-background reduction of the Lichnerowicz operator to the Laplacian is a definition, not a curved-space theorem.

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/SevenGaps/DiscreteLichnerowicz.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