continuumSymbolIs_iff
plain-language theorem explainer
The continuum-symbol predicate for a 4D integer mode, polarization matrix, and candidate value Λ is definitionally the statement that the |k|²-normalized exact midpoint Bloch symbol converges to Λ as the torus side tends to infinity. Anyone rewriting between the named Prop and an explicit filter limit cites this. The proof is pure definitional reflexivity (Iff.rfl).
Claim. For an integer wave mode $m\in\mathbb{Z}^4$, a real $4\times 4$ matrix $E$, and $\Lambda\in\mathbb{R}$, the continuum-symbol predicate holds at $(m,E,\Lambda)$ if and only if $$\frac{S^{\mathrm{exact}}_j(m,E)}{|k_j(m)|^2}\xrightarrow{j\to\infty}\Lambda,$$ where $S^{\mathrm{exact}}_j$ is the finite exact midpoint Bloch symbol on the side-$(j+3)$ Freudenthal 4-torus and $|k_j(m)|^2$ is the momentum norm squared of $m$ on that mesh.
background
This module is the first binding increment of the 4D Regge continuum-closure plan. It freezes the independent continuum target, the canonical periodic Freudenthal 4-torus mesh of side $N\ge 3$, Frobenius-normalized Euclidean TT polarizations, and honesty decoys before any continuum recovery is attempted. Nothing in the module proves that the lattice symbol recovers Einstein-Hilbert.
An integer mode $m$ is a map $\mathrm{Fin},4\to\mathbb{Z}$ (commensurate Bloch wavevector). The real covector is $k=2\pi m/N$ on side $N$. The continuum-symbol predicate asserts that the concrete exact-action finite Hessian, normalized by momentum norm squared, tends to a real value $\Lambda$ along the family $N=j+3$. The sequence is definitionally the exact midpoint Bloch symbol in the mode and polarization, not a constant face and not an existential witness; the legacy transported distinct-hinge fold is explicitly not this object.
The module tags continuum Tendsto value Props as OPEN. The frozen EH quadratic uses an independent $\kappa_{\mathrm{Einstein}}$ and must later be observed equal to the lattice symbol, never fitted.
proof idea
One-line term proof: Iff.rfl. The right-hand side is literally the body of the continuum-symbol definition, so the biconditional is definitional equality of propositions. No lemmas are applied.
why it matters
Gives a stable unfold interface between the named continuum-symbol Prop and the explicit Tendsto goal that later continuum-recovery arguments must inhabit. Downstream work (still open in this module) is charged with showing that for every nonzero integer mode and TT polarization the limit equals the scale-explicit face $(-1/8)\cdot|E|_F^2$, with pure-gauge vanishing as a separate conjunct. That open target is Restatement C of the continuum preflight; the packaged closer and S_RS_converges_EH_4d remain uninhabited.
In the broader Recognition gravity campaign this sits under the QG full-theory track: discrete Regge calculus on the eight-tick / $D=3$ spatial scaffold must recover the linearized Einstein-Hilbert quadratic in the continuum, without reverse-engineering lattice weights from the EH answer. The present lemma only freezes the geometric mesh sequence as the honest continuum object. No parent theorems yet consume it (used_by is empty).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.