Gravity Seven Gaps Discrete Lichnerowicz Discrete Eigenvalue Tendsto Raw

The lattice eigenvalue limit

The declaration discrete_eigenvalue_tendsto_raw is a theorem about a lattice approximation to a wave equation. On a lattice of points with spacing h, the discrete Laplacian is a finite-difference operator that approximates the continuous second derivative. The theorem states that for a fixed wavenumber k, the positive eigenvalue 4N²sin²(πk/N) of the discrete Laplacian on an N-point lattice tends to (2πk)² as N tends to infinity. This is the standard continuum limit: as the lattice spacing shrinks to zero, the discrete eigenvalue converges to the eigenvalue of the continuous Laplacian on a circle of circumference 1.

The result is proved in the framework's machine-checked library of formal theorems. The proof uses Fourier modes, which are complex exponentials that diagonalize the discrete Laplacian. The key identity is that the Fourier mode exp(2πikj/N) is an eigenvector of the discrete Laplacian with eigenvalue -4N²sin²(πk/N). The theorem then follows from the fact that sin(x)/x tends to 1 as x tends to 0, so 4N²sin²(πk/N) tends to 4π²k². This is a purely analytic statement about the discrete operator; it does not involve any physics beyond the definition of the lattice Laplacian.

In Recognition Science, this theorem is part of a campaign to connect discrete lattice models to continuum physics. The framework models spacetime as a discrete lattice, and this theorem shows that for plane waves along one axis, the discrete spectrum recovers the continuum spectrum in the infinite-refinement limit. The result is tagged as a THEOREM: it is proved in the library with no unproven axioms. However, the theorem is explicitly scoped to the axis sector: it applies only to plane waves traveling along one of the three coordinate axes, not to waves in arbitrary directions.

The theorem does not claim that the full discrete spectrum converges isotropically to the continuum Lichnerowicz spectrum. The framework's own documentation notes that the continuum moment tensor of the canonical frozen quadratic energy is anisotropic, with a body-diagonal direction roughly 4.9 times stiffer than an axis direction. Axis stencils are blind to this anisotropy, so the axis-sector result must not be read as isotropic flat-space recovery. The theorem also does not treat curved backgrounds such as Schwarzschild or Kerr, nor quasinormal-mode spectra; those remain open targets in the framework's status flags.

What the theorem establishes is a precise, machine-checked bridge between a discrete lattice model and a continuum operator, for a restricted class of modes. It is a building block, not a complete theory of gravity on a lattice. The reader should understand that the result is real but narrow: it proves convergence along one axis, and the framework itself flags the broader questions as open.

/-- THEOREM (raw form of the convergence, as in the campaign brief; axis
sector only, see the scope note on `discreteEigenvalue_tendsto`). -/
theorem discrete_eigenvalue_tendsto_raw (k : ℕ) :
    Filter.Tendsto
      (fun N : ℕ => 4 * (N : ℝ) ^ 2 * Real.sin (Real.pi * (k : ℝ) / (N : ℝ)) ^ 2)
      Filter.atTop (nhds ((2 * Real.pi * (k : ℝ)) ^ 2)) :=
  discreteEigenvalue_tendsto k

What this page does not claim

The theorem does not claim isotropic flat-space recovery of the full Lichnerowicz spectrum. The theorem does not treat curved backgrounds such as Schwarzschild or Kerr. The theorem does not address quasinormal-mode spectra.

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: