OperatorConvergenceStatus
plain-language theorem explainer
Status triple of booleans for the Seven-Gaps "operator convergence" lane: flat 3-torus TT axis-sector discrete-to-continuum convergence is marked proved; curved backgrounds and quasinormal-mode spectra are marked open. Gravity auditors cite it as the file's honest claim ledger. It is a pure structure definition with no proof obligations.
Claim. A record of three Boolean flags: (1) whether discrete-to-continuum operator convergence is established on the flat 3-torus for transverse-traceless axis modes $k=(k,0,0)$ of the axis-stencil Laplacian (eigenvalue identity at every resolution and spectral limit $(2\pi k)^2$); (2) whether curved backgrounds (Schwarzschild, Kerr) remain unformalized; (3) whether quasinormal-mode spectra remain unformalized.
background
Lane 4 of the Seven-Gaps gravity campaign asks whether the discrete perturbation spectrum on a lattice recovers the continuum Lichnerowicz operator. This module answers only on the flat 3-torus, representing lattice functions as $N$-periodic maps $\mathbb{Z}\to\mathbb{C}$ (spacing $h=1/N$) rather than on $\mathrm{ZMod},N$, so stencil identities hold pointwise and periodicity alone supplies the torus interpretation.
Every proved spectral statement is restricted to the AXIS stencil sector: plane waves $k=(k,0,0)$ under the componentwise axis Laplacian. Test G (Freudenthal stencil preflight / energy limit) already showed the continuum moment tensor of the frozen quadratic energy is anisotropic, $A_0=(1+\sqrt{2})I+(\sqrt{2}+\sqrt{3})J$, with body-diagonal directions roughly $4.9\times$ stiffer than axes. Axis stencils are blind to that anisotropy, so axis-sector convergence is not isotropic flat-space recovery.
The structure packages the three honest tiers of that gap as Boolean fields rather than as theorems.
proof idea
No proof: this is a structure declaration. Three named Boolean fields carry the scoped claim of the file. Downstream, a single definition instantiates all three flags (flat_tt_convergence_proved := true, the two open flags := true). The mathematical content lives in sibling lemmas (discLap_fourierMode, discreteEigenvalue_tendsto, etc.); this record only labels which tiers are closed.
why it matters
Gives the file a machine-readable claim ledger for the operator-convergence gap. The sole consumer is the module-level status definition, which sets flat TT axis convergence to proved and leaves curved backgrounds and QNM spectra open, matching the module doc's honest-tier list.
In the broader RS gravity program this sits under discrete recovery of continuum GR operators on the forced $D=3$ spatial lattice (forcing chain T8). It deliberately refuses to overclaim isotropic Lichnerowicz recovery: the anisotropic moment tensor from Test G and the C10 direction-resolved symbol probe remain the governing caveats. Curved (Schwarzschild/Kerr) backgrounds and quasinormal spectra are explicitly flagged open; nothing elsewhere in the repository closes them.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.