module module high

`IndisputableMonolith.Gravity.SevenGaps.DiscreteLichnerowicz`

Defines the spacing-normalized 1D discrete Laplacian on N cyclic lattice sites and diagonalizes it in Fourier modes, with eigenvalues tending to the continuum Laplacian spectrum. QG seven-gaps workers cite it as the certified flat-spectrum kernel behind Gap 4. The argument is Fourier eigenfunction calculus plus a standard continuum limit of the discrete eigenvalues.

claimOn the cyclic lattice of $N$ sites with spacing $h=1/N$, the discrete Laplacian acts by $(\Delta_h f)_j=(f_{j+1}-2f_j+f_{j-1})/h^2$. Fourier modes $e^{2\pi i kj/N}$ are eigenfunctions with eigenvalues $-(4/h^2)\sin^2(\pi k/N)$, which tend to $-(2\pi k)^2$ as $N\to\infty$. Continuum Lichnerowicz is taken as the flat reduction $\Delta_L=-\Delta$.

background

This module sits in the Gravity seven-gaps campaign: a machine-checked ledger of scoped quantum-gravity increments that deliberately stop short of full physical closure. The local object is a spacing-normalized discrete Laplacian on the unit circle. For a function $f$ on $N$ sites with $h=1/N$,

$(\mathrm{discLap},f)_j=(f(j+1)-2f(j)+f(j-1))/h^2$.

Fourier modes on the cyclic lattice are the natural eigenbasis. The continuum Lichnerowicz operator is introduced only through the flat identification $\Delta_L=-\Delta$; there is no curvature endomorphism in the definitions. Downstream Gap-4 analysis treats these as axis modes of a componentwise flat lattice Laplacian, not a curved-background operator.

proof idea

Definition-and-spectrum module, not a single theorem. It introduces discLap and the cyclic Fourier modes, records periodicity and step relations, and proves the discrete Laplacian acts by multiplication on each mode (via the elementary identity for $e^{i\theta}+e^{-i\theta}$). Discrete eigenvalues are packaged as a named quantity; a tendsto lemma then sends those eigenvalues to the continuum Laplacian values as $N\to\infty$. Supporting arithmetic (complex exponential addition) is local. No curvature or higher-dimensional coupling enters the proofs.

why it matters in Recognition Science

Supplies the certified flat discrete spectrum that the seven-gaps campaign records and that Gap 4 explicitly bounds. CampaignLedger imports it as a scoped, kernel-checked increment without flipping any full-strength QGScopeAudit flag. CurvedOperatorUnderdetermination quotes the narrow reach directly: the spectrum theorem treats axis modes of the componentwise flat lattice Laplacian, introduces continuum Lichnerowicz only from $\Delta_L=-\Delta$, and contains no Riemann-curvature endomorphism, so it cannot fix a curved-background coupling. In the Recognition gravity stack this is the honest flat kernel against which underdetermination of curvature coupling is stated.

scope and limits

Does not include a Riemann-curvature endomorphism or any curved-background coupling.
Does not certify a full Lichnerowicz spectrum on a Riemannian manifold; only flat cyclic 1D (axis) modes.
Does not flip any QGScopeAudit full-strength closure flag in the seven-gaps ledger.
Does not identify discrete eigenvalues with physical graviton or spin-2 masses.
Continuum Lichnerowicz value is definitional from $\Delta_L=-\Delta$, not derived from curvature.

used by (2)

From the project-wide theorem graph. These declarations reference this one in their body.

IndisputableMonolith.Gravity.SevenGaps.CampaignLedger module_import
IndisputableMonolith.Gravity.SevenGaps.CurvedOperatorUnderdetermination module_import

declarations in this module (50)

def discLap L88
def fourierMode L93
theorem fourierMode_periodic L98
lemma fourierMode_step L114
lemma fourierMode_step_down L125
lemma exp_add_exp_neg_mul_I L136
theorem discLap_fourierMode_apply L147
theorem discLap_fourierMode L190
def discreteEigenvalue L201
theorem discreteEigenvalue_tendsto L219
theorem discrete_eigenvalue_tendsto_raw L274
abbrev Site3 L283
abbrev LatticeTensorField L286
def unitVec L289
lemma fst_add_e0 L294
lemma fst_sub_e0 L295
lemma fst_add_e1 L296
lemma fst_sub_e1 L297
lemma fst_add_e2 L298
lemma fst_sub_e2 L299
def discDiv L303
def discLap3 L307
def planeH L314
lemma planeH_apply L318
theorem planeH_periodic_axis L325
theorem planeH_shift_yz L333
theorem planeH_transverse L343
theorem discLap3_planeH L353
def epsPlus L369
def epsCross L372
theorem epsPlus_isSymm L374
theorem epsCross_isSymm L378
theorem epsPlus_traceless L382
theorem epsCross_traceless L387
theorem epsPlus_row0 L392
theorem epsCross_row0 L396
theorem epsPlus_col0 L400
theorem epsCross_col0 L404
theorem polarizations_linearIndependent L410
def continuumProfile L432
def continuumPlaneH L436
theorem continuumProfile_hasDerivAt L441
theorem continuumProfile_second_deriv L457
def lichnerowiczFlatEigenvalue L484
theorem discrete_tt_spectrum_converges_to_flat_lichnerowicz L514
structure OperatorConvergenceStatus L535
def status L557
theorem status_flat_tt_convergence_proved L562
theorem status_curved_background_open L565
theorem status_qnm_spectrum_open L568