finiteExactReggeSymbol_zero
plain-language theorem explainer
On the zero strain matrix the exact flat Regge cross-term continuum symbol vanishes for every torus side and Bloch mode. Gravity analysts tracking the H_fold continuum pivot cite this as the zero-amplitude baseline of the bare s''_Regge face. The proof is a one-line reduction through scalar homogeneity at scale zero.
Claim. For every torus side index $j\in\mathbb{N}$ and every integer Bloch mode $m\in\mathbb{Z}^4$, the exact flat Regge cross-term continuum symbol on the zero $4\times 4$ strain matrix is zero: $S''_j(m;0)=0$.
background
This module isolates the exact flat cross-term continuum symbol that the H_fold oracle binds to: at a flat background, hinge deficits vanish, so Schläfli reduces the Regge Hessian to the bare cross term $S''=\sum_h(dA_h)(d\delta_h)$. The named sequence finiteExactReggeSymbol evaluates that geometry-derived fold on plane-wave class strains at torus side $j$ and integer mode $m$, before any discrete bookkeeping factor.
Deficits here are the usual hinge quantities $2\pi-\sum\theta$ (DihedralAngle / Schläfli). The fold phases star-member cubes with position-resolved origins so that normalized TT on the banked directions hits $-1/4$. The continuum-preflight layer re-exports this symbol as the face that ContinuumSymbolIs is meant to tend to.
A sibling homogeneity lemma records how the symbol scales under real multiples of the strain matrix; the zero-strain identity is the scale-zero corner of that relation.
proof idea
One-line wrapper. Apply the scalar-homogeneity lemma finiteExactReggeSymbol_smul at scale $c=0$ on the unit matrix strain: the left-hand side becomes the symbol at $0\cdot I=0$, and the right-hand side is identically zero. simpa closes the equality.
why it matters
Structural baseline for the MODEL object finiteExactReggeSymbol / exactFlatCrossTermFold in the H_fold pivot. Oracle verdict (2026-07-21): 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 not the continuum object. Zero-strain vanishing is the first sanity check before edge-origin $m^2$ certificates and continuum Tendsto statements.
No downstream Lean users are wired yet (used_by empty). It supports the THEOREM tier of structural lemmas (homogeneity, zero-momentum member drop, status flags) that Preflight and the banked Hessian symbol modules rely on. Open items it does not close: FoldAlongM2Tendsto / ContinuumSymbolIs for all modes, ledger $S_{RS}$ inhabit, and $e_0$ isotropy remain open; it also does not flip transportedGaugeZeroClosed.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.