finiteExactReggeSymbolSequence
plain-language theorem explainer
Re-export of the exact flat cross-term Regge symbol as a sequence over mesh index j, for fixed integer Bloch mode m and polarization matrix E. Continuum-preflight and EH-recovery arguments cite it as the geometric mesh sequence whose |k|²-normalized limit is the frozen Einstein-Hilbert target. The body is a one-line alias of the definition in Regge4DExactActionSymbol.
Claim. For each integer mode $m:\{0,1,2,3\}\to\mathbb{Z}$ and each $4\times 4$ real matrix $E$, the finite exact Regge symbol sequence is the map $j\mapsto S^{\mathrm{exact}}_j(m,E)\in\mathbb{R}$, where $S^{\mathrm{exact}}_j$ is the exact flat cross-term Regge action symbol on the $j$-th mesh refinement.
background
This module is the first binding increment of the 4D continuum closure plan in the QG full-theory campaign. It freezes the independent continuum target, canonical mesh carrier, normalized TT data, pure-gauge family, and honesty decoys before further computation. Nothing in the module proves continuum recovery.
The canonical carrier is a periodic Freudenthal 4-torus of side $N\ge 3$. The continuum object of record is the exact flat cross-term symbol coming from exactFlatCrossTermFold, not the legacy distinct-hinge transport fold (retained only for comparison). The sequence form packages that symbol as a function of mesh index so later Tendsto statements can treat refinement as $j\to\infty$.
Upstream, finiteExactReggeSymbolSequence is defined by pointwise evaluation: $j\mapsto$ the exact finite symbol at level $j$ on mode $m$ and matrix $E$. Sibling objects in this file fix Mat4, wave modes, momentum norms, and the canonical torus.
proof idea
One-line abbreviation. The declaration simply names the already-defined sequence from Regge4DExactActionSymbol, with no extra hypotheses, coercions, or algebraic work. Downstream proofs that need the sequence in the preflight namespace resolve to that upstream def.
why it matters
Preflight freezes the geometric mesh sequence that the open continuum target compares to the independently defined linearized Einstein-Hilbert quadratic (using kappa_einstein, not a fitted lattice scale). Module tags mark continuum Tendsto Props and S_RS_converges_EH_4d as OPEN; this abbrev supplies the left-hand geometric object those Props will quantify over.
It keeps the exact-fold symbol (not bare blochFoldAll, not fitted $2/r$, not the mis-transporting distinct-hinge fold) as the named continuum sequence inside the gravity analysis stack. Parent use is the same symbol package in Regge4DExactActionSymbol; the preflight re-export makes that sequence available beside Frobenius pin lemmas, decoy discriminators, and the frozen EH functional without reverse-engineering lattice weights from the EH answer.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.