discreteExactReggeSymbolSequence
plain-language theorem explainer
Packages the discrete exact Regge symbol (bookkeeping factor times the finite flat cross-term fold) as a sequence in the lattice scale index, at fixed Bloch mode and strain matrix. Gravity analysts writing continuum-symbol Tendsto or Preflight bindings against the discrete Hessian would cite it. The body is a one-line eta-expansion of the pointwise symbol.
Claim. For integer Bloch wavevector $m\in\mathbb{Z}^4$ and real $4\times 4$ strain matrix $E$, the assignment $j\mapsto$ (discrete bookkeeping factor) times the finite exact flat cross-term Regge fold at scale $j$, mode $m$, and strain $E$, defines a sequence $\mathbb{N}\to\mathbb{R}$.
background
This module isolates the exact flat cross-term continuum symbol for the Regge action Hessian on the Freudenthal torus (oracle pivot $H_{\mathrm{fold}}$). At flat background, deficits vanish, so Schläfli reduces the second variation to the cross term $S''=\sum_h(dA_h)(d\delta_h)$, evaluated on plane-wave class strains with position-resolved deficit phasing.
Mat4 is the real $4\times 4$ matrix type for strain tensors. The pointwise discrete exact symbol is the 3D-parallel bookkeeping package: twice the finite exact flat cross-term fold at lattice scale $j$, Bloch integers $m$, and strain $E$. The ledger continuum-symbol interface currently binds the bare finite fold sequence; the factor-of-two form is the alternate geometric continuum sequence normalized by $|k|^2$.
Upstream edge-index abbreviations (E from lattice-ball and Freudenthal strip modules) supply the discrete geometry scaffolding used by the hinge and star-kernel assembly that feeds the finite fold.
proof idea
One-line definitional wrapper: the sequence is the eta-expansion $j\mapsto$ discrete exact Regge symbol at $(j,m,E)$. No tactics, no lemmas; pure function abstraction over the already-defined pointwise package (bookkeeping factor times finite exact fold).
why it matters
Gives the sequence-shaped handle needed for continuum-limit statements (Tendsto of the discrete symbol along lattice refinements) in the exact flat Hessian analysis. The module tags FoldAlongM2Tendsto / geometric ContinuumSymbolIs Tendsto for all modes as OPEN; Preflight currently binds ContinuumSymbolIs to the bare finite-fold sequence, not this bookkeeping-scaled form.
No downstream consumers are wired yet (used_by empty). It sits beside the structural lemmas (homogeneity, zero-momentum member drop) and the banked edge-origin $m^2$ certificates for axisTTPlus / axisTTCross / decoy gauge families on symbolDir. Does not close ledger $S_{RS}$ inhabit or gap_action_recovery, and does not flip the fold-internal gauge-zero flag. Framework role is local to 4D Regge Hessian continuum matching, not the T0–T8 forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.