finiteExactReggeSymbolSequence
plain-language theorem explainer
Packages the exact flat Regge cross-term symbol as a sequence over lattice resolution j, at fixed Bloch mode m and strain matrix E. Continuum-limit preflight and Tendsto arguments cite this packaging rather than the pointwise map. The body is a one-line eta-expansion of the pointwise finite exact symbol.
Claim. For a mode multi-index $m\in\mathbb{Z}^4$ and a $4\times 4$ real strain matrix $E$, define the sequence $j\mapsto S^{\mathrm{exact}}_j(m,E)$ of finite-lattice exact flat Regge cross-term symbols at resolution $j\in\mathbb{N}$.
background
This module isolates the exact flat cross-term continuum symbol (oracle tag H_fold). On a flat background, deficits vanish, so Schläfli reduces the Hessian cross term to $S''=\sum_h (dA_h)(d\delta_h)$. The binding object is that Hessian on plane-wave class strains with position-resolved deficit phasing: t11 keeps star-member cube offsets; t12/t13/t22 use per-edge transported origins.
Mat4 is the abbreviation for $4\times 4$ real matrices (strain data). The pointwise map finiteExactReggeSymbol is the MODEL-tier geometry-derived flat cross-term at fixed resolution j, mode m, and strain E; it is not yet Schläfli-elevated from the full nonlinear action for every orbit. Spatial dimension D=3 is the forced RS value (T8), matching the 4D spacetime lattice setting (3 space + time).
The continuum preflight layer binds ContinuumSymbolIs to Tendsto of this sequence, not to a constant face value. Discrete bookkeeping parallels the 3D convention $ttSecondDifference=(2/N^3)\cdot S''$.
proof idea
One-line definitional wrapper: the sequence is the eta-expansion $j\mapsto$ pointwise exact flat Regge symbol at $(j,m,E)$. No lemmas, no tactics; pure packaging so analysis can quantify over resolution.
why it matters
Gives the continuum preflight module a named $\mathbb{N}\to\mathbb{R}$ object to feed Tendsto statements. Downstream, Regge4DContinuumPreflight re-exports this sequence as its binding face for ContinuumSymbolIs.
In the H_fold story, the true Regge Hessian on the Freudenthal torus annihilates vertex-gauge modes and sends normalized TT on axisTTPlus/symbolDir to $-1/4$. The distinct-hinge transported fold is explicitly not the continuum object. This sequence is the MODEL-tier carrier for the geometry-derived flat cross-term that those continuum claims target.
Open items it sits under: FoldAlongM2Tendsto / geometric ContinuumSymbolIs Tendsto for all modes; ledger $S_{RS}$ inhabit; e0 isotropy. It does not close gap_action_recovery or flip transportedGaugeZeroClosed.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.