Encyclopedia Gravity Gravity Seven Gaps Discrete Lichnerowicz Discrete Eigenvalue Tendsto

ARTICLE 4 claims 3 theorems 1 model

Gravity Seven Gaps Discrete Lichnerowicz Discrete Eigenvalue Tendsto

A machine-checked proof shows that a certain discrete eigenvalue on a lattice converges to the continuum value as the lattice is refined, but only along one axis.

Verify this page

The lattice limit

In numerical analysis, a common sanity check is to see whether a discrete approximation to a differential operator reproduces the known continuum result as the grid spacing goes to zero. The theorem discreteEigenvalue_tendsto performs this check for a specific operator. It proves that for a fixed wavenumber k, the eigenvalue of the discrete Laplacian on a one-dimensional lattice of spacing 1/N, given by 4N²sin²(πk/N), converges to (2πk)² as N tends to infinity. This is the standard discrete-to-continuum limit for a plane wave.

The result is part of a larger effort to connect a discrete model of spacetime to the continuous theory of general relativity. The framework's machine-checked library of formal theorems establishes that this convergence holds for the axis-aligned plane wave, where the wave travels along one coordinate axis. The proof also shows that the continuum plane wave exp(2πikt) has second derivative -(2πk)² times itself, confirming that (2πk)² is the genuine eigenvalue of the continuum minus-Laplacian along that direction. On a flat background, the Lichnerowicz operator, which governs gravitational perturbations, reduces to this minus-Laplacian, so the discrete eigenvalues converge to the flat-space gravitational eigenvalue.

In Recognition Science, this is a step toward showing that a discrete ledger of events can reproduce the continuous equations of gravity. The theorem is proved in the framework's library, which is a machine-checked collection of formal theorems. It is one of seven gaps in the framework's gravity program, specifically the operator convergence gap. The proof is axiom-clean, meaning it relies only on the standard axioms of the underlying type theory.

The scope is deliberately narrow. The convergence is proved only for the axis stencil, a discretization scheme that uses only neighboring points along the coordinate axes. The framework's own tests have shown that this stencil is anisotropic, meaning it treats different spatial directions differently. The body-diagonal direction is roughly 4.9 times stiffer than an axis direction. Therefore, the axis-sector result must not be read as a full recovery of the isotropic flat-space Lichnerowicz spectrum. The direction-resolved symbol question remains open.

The theorem does not address curved backgrounds. The status flags in the library explicitly mark curved backgrounds, such as Schwarzschild or Kerr, and quasinormal-mode spectra as open. The result is a sector statement, not a general proof of discrete-to-continuum convergence for all of gravity.

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 continuumProfile_second_deriv · IndisputableMonolith/Gravity/SevenGaps/DiscreteLichnerowicz.lean
continuumProfile_second_deriv · IndisputableMonolith/Gravity/SevenGaps/DiscreteLichnerowicz.lean:453 
/-- THEOREM. Second derivative of the continuum profile: `-(2πk)²` times the
profile. So `(2πk)²` is the genuine `-d²/dt²` eigenvalue of the continuum
mode along the wave direction (the mode is constant in the transverse
directions). -/
theorem continuumProfile_second_deriv (k : ℕ) (t : ℝ) :
    HasDerivAt (fun s : ℝ => 2 * (Real.pi : ℂ) * Complex.I * (k : ℂ) * continuumProfile k s)
      (((-((2 * Real.pi * (k : ℝ)) ^ 2) : ℝ) : ℂ) * continuumProfile k t) t := by
  have h := (continuumProfile_hasDerivAt k t).const_mul
    (2 * (Real.pi : ℂ) * Complex.I * (k : ℂ))
  have heq : ((-((2 * Real.pi * (k : ℝ)) ^ 2) : ℝ) : ℂ) * continuumProfile k t
      = 2 * (Real.pi : ℂ) * Complex.I * (k : ℂ)
        * (2 * (Real.pi : ℂ) * Complex.I * (k : ℂ) * continuumProfile k t) := by
    push_cast
    linear_combination (-4 * (Real.pi : ℂ) ^ 2 * (k : ℂ) ^ 2 * continuumProfile k t)
      * Complex.I_sq
  rw [heq]
  exact h
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 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

What this page does not claim

The theorem does not prove convergence for all spatial directions, only for the axis-aligned plane wave. The result does not address curved backgrounds or quasinormal-mode spectra, which remain open. The definition of the flat Lichnerowicz eigenvalue is a model, 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