Pith. sign in
module module high

IndisputableMonolith.Gravity.SevenGaps.CurvedOperatorUnderdetermination

show as:
view Lean formalization →

A one-parameter family of lattice tensor-field operators couples the certified flat discrete Laplacian to a zeroth-order scalar curvature term. Distinct extensions agree on the entire flat specialization yet diverge at nonzero curvature, so flat spectral data underdetermine the curved operator. Gravity and QG campaign readers cite it when auditing the operator-convergence gap. The argument is constructive comparison of single- and double-curvature extensions plus spectral limits from the analysis toolkit.

claimA one-parameter family of lattice operators $L_\kappa=-\Delta_3^{\mathrm{disc}}+\kappa\,S$ on tensor fields, where $-\Delta_3^{\mathrm{disc}}$ is the certified positive flat discrete Laplacian and $S$ is a zeroth-order scalar curvature coupling. Distinct extensions agree on the whole flat specialization ($S=0$) yet differ at nonzero curvature. Curved discrete eigenvalues along plane-wave modes tend to continuum counterparts in the spectral-toolkit sense; the family is a countermodel, not the physical curved Lichnerowicz operator.

background

The Seven-Gaps campaign, Lane 4, targets operator convergence between discrete lattice spectra and continuum Lichnerowicz operators. Upstream, DiscreteLichnerowicz already connects the discrete perturbation spectrum on a lattice to the continuum Lichnerowicz operator on the flat 3-torus background, without importing the older vacuous Relativity/GW files. SpectralConvergence supplies the quantitative eigenvalue-limit toolkit (Phase 2a of the QG full-theory campaign), theorem-status and axiom-clean.

This module does not define the physical curved Lichnerowicz operator. Per its doc-comment it introduces a countermodel family: the first term is the certified positive flat operator $-\mathrm{discLap3}$; the second is a zeroth-order scalar curvature coupling. Sibling constructions include single- and double-curvature extensions, a constant-plus-field test configuration annihilated by the discrete Laplacian, flat-specialization agreement, distinction at nonzero curvature, and plane-wave curved discrete/continuum eigenvalues with a tendsto limit.

proof idea

The module builds an explicit one-parameter curvature-coupled operator and two extensions (single and double curvature). It proves they specialize identically when curvature vanishes (agreement on the entire flat sector) yet are distinct at nonzero curvature. Auxiliary facts: the discrete Laplacian kills constant-plus-field configurations; the coupled operator recovers the flat operator on the flat specialization. On the spectral side, curved discrete eigenvalues are defined, matched to continuum eigenvalues on plane-wave modes, and shown to converge via the SpectralConvergence toolkit. Overall shape: constructive countermodel, specialization lemmas, and limit lemmas, not a uniqueness theorem.

why it matters in Recognition Science

FullTheoryLedger imports this module into the live benchmark ledger of the full quantum-gravity theory campaign. That ledger holds one boolean flag per pillar benchmark and flips a flag only when the target is kernel-checked, axiom-audited, and critic-passed. By exhibiting underdetermination (flat spectral agreement does not pin a unique curved extension), the module sharpens what Lane 4 still needs beyond the flat 3-torus DiscreteLichnerowicz result. It is deliberately a countermodel family, so it bounds uniqueness claims about curved discrete operators rather than closing a physical curved Lichnerowicz definition. Campaign auditors use it when checking whether flat-certified positivity and spectral limits alone select curved gravity operators.

scope and limits

used by (1)

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

depends on (2)

Lean names referenced from this declaration's body.

declarations in this module (22)