finiteExactReggeSymbol_smul
plain-language theorem explainer
The exact flat Regge continuum symbol on a finite torus is homogeneous of degree two in the strain matrix: scaling the 4×4 class strain by a real constant multiplies the symbol by the square of that constant. Anyone assembling continuum-limit or discrete bookkeeping identities for the H_fold pivot cites this. The proof is a one-line unfold plus the corresponding homogeneity lemma for the underlying cross-term fold.
Claim. For every real scalar $c$, torus level $j\in\mathbb{N}$, integer wave covector $m:\mathrm{Fin}\,4\to\mathbb{Z}$, and $4\times 4$ real strain matrix $E$, the exact flat Regge continuum symbol satisfies $\sigma_j(m,cE)=c^2\,\sigma_j(m,E)$, where $\sigma_j(m,\cdot)$ is the bare cross-term fold evaluated on the real plane-wave mode with frequencies $2\pi m_i/L_j$.
background
This module isolates the exact flat cross-term continuum symbol that the oracle tags as the true Regge Hessian pivot $H_{\mathrm{fold}}$ on the Freudenthal torus. At flat background, deficits vanish, so Schläfli reduces the second variation to the bilinear cross term $S''=\sum_h(dA_h)(d\delta_h)$. The named sequence finiteExactReggeSymbol evaluates that fold on plane-wave class strains with position-resolved deficit phasing.
A strain is a real $4\times 4$ matrix (Mat4). The mode fed to the fold is familyRealMode j m, the real covector with components $2\pi m_i$ over the side length of torus level $j$. The continuum symbol is then just the exact flat cross-term fold of $E$ against that mode: bare $s''_{\mathrm{Regge}}$ before any discrete bookkeeping factor.
Upstream, homogeneity of degree two is already proved for the fold itself (exactFlatCrossTermFold_smul): each slot contribution scales as $c^2$ because both area and deficit variations are linear in the strain.
proof idea
One-line wrapper. Unfold the definition of the finite exact symbol (it is exactly the cross-term fold on familyRealMode j m), then apply exactFlatCrossTermFold_smul at scalar $c$, matrix $E$, and wave $m$ equal to that family mode. No extra algebra is needed; the $c^2$ factor is inherited verbatim from the fold.
why it matters
Homogeneity is structural scaffolding for the $H_{\mathrm{fold}}$ story: the continuum symbol must behave as a quadratic form on strains so that TT normalizations and gauge annihilations are scale-consistent. Downstream, discreteExactReggeSymbol_smul lifts the same $c^2$ law through the discrete bookkeeping factor by rewriting with this lemma, and finiteExactReggeSymbol_zero obtains vanishing at the zero matrix by specializing $c=0$.
In the module's tier tags this sits among the THEOREM structural lemmas (homogeneity, zero-momentum drop, status flags) that support the MODEL object finiteExactReggeSymbol. It does not close the open continuum tendsto goals (FoldAlongM2Tendsto, geometric ContinuumSymbolIs) nor the ledger $S_{RS}$ inhabit, but it keeps the quadratic face of the bare Regge cross-term clean for those later limits.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.