Encyclopedia Gravity Gravity Seven Gaps Discrete Lichnerowicz

ARTICLE 5 claims 4 theorems 1 model

Gravity Seven Gaps Discrete Lichnerowicz

A machine-checked proof that lattice vibrations on a flat 3-torus converge to the continuum gravity operator, with an honest scope limit.

Verify this page

The discrete spectrum bridge

The Lichnerowicz operator is the linearized gravity operator that governs how small perturbations of the metric evolve on a curved background. In the flat case, on a torus with no curvature, this operator reduces to the ordinary Laplacian, the sum of second derivatives along each spatial direction. The module Seven-Gaps campaign, a framework program to close seven identified gaps in its gravity formalism, targets the operator convergence gap: showing that a discrete lattice version of this operator approaches the continuum one as the lattice spacing shrinks.

The classical setup is a 3-torus, a cube with opposite faces identified, with lattice spacing h = 1/N. The module represents lattice functions as N-periodic functions on the integers, avoiding wraparound arithmetic. The core theorem discreteEigenvalue_tendsto proves that for a fixed wavenumber k, the discrete eigenvalue 4N²sin²(πk/N) of the axis-mode Laplacian converges to (2πk)² as N → ∞, which is exactly the continuum eigenvalue. The proof uses Fourier modes, showing that exp(2πikj/N) is an eigenvector of the discrete Laplacian with that eigenvalue, and then taking the limit.

The module also establishes the transverse-traceless (TT) polarization structure. It defines the two standard polarizations ε⁺ and ε×, proves they are symmetric, traceless, have zero first row and column, and are linearly independent. The axis plane wave with first-row-zero polarization is exactly discrete-transverse, meaning its forward-difference divergence vanishes identically. The 3D axis plane wave is an eigenvector of the 3D discrete Laplacian with the same eigenvalue as the 1D mode, and the continuum profile has the correct second derivative.

In Recognition Science, the framework models the flat Lichnerowicz eigenvalue as (2πk)² via the definition lichnerowiczFlatEigenvalue, justified because the Riemann curvature term vanishes on a flat background. The packaged claim, discrete_tt_spectrum_converges_to_flat_lichnerowicz, states that discrete TT eigenvalues of axis modes converge to this flat eigenvalue. This is the first genuine Lean connection between the discrete perturbation spectrum and the continuum Lichnerowicz operator.

The scope is explicit and honest. Every convergence result is proved along the axis stencil sector only, for plane waves k = (k, 0, 0). Test G kernel-proved that the continuum moment tensor is anisotropic, with the body-diagonal direction roughly 4.9 times stiffer than an axis direction. Axis stencils are blind to this anisotropy, so the results must not be read as isotropic flat-space recovery. Curved backgrounds (Schwarzschild, Kerr) and quasinormal-mode spectra remain open, as recorded in the status flags. The framework proves a sector statement, not a full recovery.

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 discLap_fourierMode · IndisputableMonolith/Gravity/SevenGaps/DiscreteLichnerowicz.lean
discLap_fourierMode · IndisputableMonolith/Gravity/SevenGaps/DiscreteLichnerowicz.lean:188 
/-- THEOREM (eigenvalue identity, function form).
`discLap (fourierMode k) = -(4 N² sin²(πk/N)) • fourierMode k`. -/
theorem discLap_fourierMode (N : ℕ) (k : ℤ) :
    discLap N (fourierMode N k)
      = (-(4 * (N : ℝ) ^ 2 * Real.sin (Real.pi * (k : ℝ) / (N : ℝ)) ^ 2)) • fourierMode N k := by
  funext j
  rw [Pi.smul_apply, Complex.real_smul]
  exact discLap_fourierMode_apply N k j
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
MODEL lichnerowiczFlatEigenvalue · IndisputableMonolith/Gravity/SevenGaps/DiscreteLichnerowicz.lean
lichnerowiczFlatEigenvalue · IndisputableMonolith/Gravity/SevenGaps/DiscreteLichnerowicz.lean:471 
/-- MODEL. Flat-background Lichnerowicz eigenvalue on the wavenumber-`k` TT
plane wave: `(2πk)²`.

Justification (why this is the honest definition): the Lichnerowicz operator
on a Ricci-flat background acts on TT perturbations as
`Δ_L h_ab = -∇² h_ab - 2 R_acbd h^cd`. On the FLAT 3-torus the Riemann
tensor vanishes identically, so `Δ_L` reduces to `-∇²` (minus the flat
Laplacian) on TT tensors. The TT plane wave with wavenumber `k` along an
axis of the unit torus has `-∇²` eigenvalue `(2πk)²`; the along-axis part of
this is PROVED above (`continuumProfile_second_deriv`), and the transverse
derivatives vanish because the mode is constant in `y, z`. No curved-space
geometry is formalized here; this definition encodes the flat reduction
only. -/
noncomputable def lichnerowiczFlatEigenvalue (k : ℕ) : ℝ :=
  (2 * Real.pi * (k : ℝ)) ^ 2
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

What this page does not claim

This does not claim isotropic flat-space recovery of the full Lichnerowicz spectrum. This does not claim any result for curved backgrounds or quasinormal-mode spectra. This does not claim the discrete Laplacian stencil is isotropic.

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