Regge4DContinuumSymbolIs
plain-language theorem explainer
Packages the continuum-limit predicate for the 4D Regge exact-action Hessian: the |k|²-normalized midpoint Bloch symbol on the side-(j+3) torus tends to Λ for integer mode m and polarization matrix E. Gravity continuum-closure work cites it as the geometric binder for EH and gauge-zero targets. Body is a pure Tendsto definition, not a proved limit.
Claim. For an integer 4-mode $m\in\mathbb{Z}^4$, a real $4\times 4$ matrix $E$, and $\Lambda\in\mathbb{R}$, write $\mathrm{Regge4DContinuumSymbolIs}(m,E,\Lambda)$ when $$\frac{S_j(m,E)}{|k_j(m)|^2}\xrightarrow{j\to\infty}\Lambda,$$ where $N_j=j+3$, $k_j=2\pi m/N_j$, and $S_j$ is the exact midpoint Bloch symbol of the flat Regge Hessian on the periodic Freudenthal 4-torus of side $N_j$.
background
Module Regge4DContinuumPreflight freezes the independent continuum target for the QG 4D campaign before any recovery proof. The carrier is the canonical periodic Freudenthal 4-torus of side $N\ge 3$, with continuum family $N=j+3$. Integer modes $m:\mathrm{Fin},4\to\mathbb{Z}$ are commensurate wave vectors; the real covector is $k=2\pi m/N$, and momentumNormSq is $|k|^2$ via the wave-norm square.
The numerator sequence is finiteExactMidpointBlochSymbol: the exact flat Hessian midpoint Bloch symbol evaluated at that real mode. Doc-comment insists the sequence is the concrete exact-action mesh symbol (definitionally tied to $E$), not a constant face, not an existential witness, and not the legacy distinct-hinge transported fold.
Local setting: MODEL/DEFINITION tier. Nothing here proves continuum recovery; OPEN targets later assert that the limit equals the frozen EH face on TT polarizations and vanishes on pure gauge.
proof idea
Definitional wrapper only. The predicate is exactly Tendsto of
j ↦ finiteExactMidpointBlochSymbol j m E / momentumNormSq (torusSide j) m
along atTop into the neighborhood filter of $\Lambda$. No lemmas are applied; torusSide j = j+3 and the midpoint Bloch rebound supply the mesh sequence. Downstream continuumSymbolIs_iff is the corresponding unfold theorem.
why it matters
This is the geometric mesh binder for the entire 4D continuum preflight. Open targets Regge4DContinuumEHTarget and Regge4DContinuumGaugeZeroTarget quantify over it: TT modes should hit the scale-explicit EH face $(-1/8)|E|_F^2$, pure gauge should hit $0$. Uniqueness (continuumSymbolIs_unique) and the iff-unfold sit on top of the same Prop.
Downstream, Regge4DPlusCrossAgreeTarget asks plus/cross polarizations to share one continuum value; torus continuum-limit and algebraic-closer modules consume the predicate as the honesty contract. Module doc tags continuum Tendsto Props OPEN and stresses that banked algebraic faces ($2\cdot(-1/8)=-1/4$, gauge $0$) must not inhabit these geometric Props. Landmark link: D=3 spatial plus time gives the 4D Regge mesh whose weak-field continuum should recover linearized EH, without reverse-engineering lattice weights from the EH answer.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.