status
plain-language theorem explainer
Status certificate for the Seven-Gaps operator-convergence lane: flat 3-torus TT convergence is marked proved on the axis stencil sector only, while curved backgrounds and quasinormal-mode spectra stay open. Gravity auditors cite it to read campaign state without opening the spectral lemmas. The body is a three-field record literal over OperatorConvergenceStatus, not a proof.
Claim. The operator-convergence status record sets three flags: flat $3$-torus transverse-traceless convergence along axis modes $k=(k,0,0)$ is proved; curved-background formalization (Schwarzschild, Kerr) is open; quasinormal-mode spectra are open. Axis-sector proved does not mean isotropic flat-space recovery of the full Lichnerowicz spectrum.
background
Module setting is Seven-Gaps Lane 4 (operator convergence): the first Lean link between a discrete lattice perturbation spectrum and the continuum Lichnerowicz operator, restricted to the flat unit $3$-torus. Lattice functions are $N$-periodic maps $\mathbb{Z}\to\mathbb{C}$ with spacing $h=1/N$, not ZMod N, so stencil identities hold pointwise and periodicity alone supplies the torus reading.
Every proved spectral fact in the file is axis-sector only: plane waves $k=(k,0,0)$ under the componentwise axis-stencil Laplacian. Test G (Freudenthal stencil preflight / energy limit) showed the continuum moment tensor of the frozen quadratic energy is anisotropic, $A_0=(1+\sqrt{2})I+(\sqrt{2}+\sqrt{3})J$, so axis stencils cannot be read as isotropic flat recovery. The direction-resolved symbol question is deferred to the C10 probe.
OperatorConvergenceStatus packages three booleans: flat TT axis convergence proved; curved backgrounds open; QNM spectra open. Sibling lemmas (discLap_fourierMode, discreteEigenvalue_tendsto) discharge the first flag; nothing in-repo formalizes the other two.
proof idea
Definition, not a theorem. The body is a structure literal of type OperatorConvergenceStatus with three boolean fields set by hand: flat_tt_convergence_proved := true, curved_background_open := true, qnm_spectrum_open := true. No tactics, no lemmas applied at this site; the true flag is justified only by the axis-sector spectral theorems proved earlier in the same module.
why it matters
Closes the bookkeeping face of Seven-Gaps Lane 4: auditors and downstream status aggregators can see that discrete-to-continuum Lichnerowicz convergence is claimed only for flat $T^3$ TT axis modes, with eigenvalue identity at every resolution and spectral limit $(2\pi k)^2$ on that sector. Parent consumers in the graph are mostly cross-module status readers and certificates; the scientific payload is the honest split between proved axis-sector flat TT work and the still-open curved-background and QNM lanes.
Framework role: gravity-side continuum limit of recognition geometry on the eight-tick / $D=3$ lattice, without importing the vacuous legacy Relativity/ GW stubs. Does not touch T5 J-uniqueness or the RCL directly; it records how far the discrete operator story has been forced toward continuum GR on the flat torus. Open questions it surfaces: isotropic (non-axis) symbol recovery under the anisotropic Freudenthal moment tensor, and any Lean treatment of Schwarzschild/Kerr or QNM spectra.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.