discreteExactReggeSymbol_smul
plain-language theorem explainer
The discrete exact Regge symbol is homogeneous of degree two in the strain matrix: scaling the 4×4 strain by a real constant multiplies the symbol by the square of that constant. Continuum-limit and Hessian-scaling arguments for the flat Regge cross term cite this. The proof unfolds the bookkeeping factor, rewrites by the finite-symbol smul lemma, and closes by ring.
Claim. For every real scalar $c$, resolution index $j\in\mathbb{N}$, integer Bloch mode $m:\{0,1,2,3\}\to\mathbb{Z}$, and real $4\times 4$ strain matrix $E$, the discrete exact Regge symbol (bookkeeping factor times the finite flat cross-term fold) satisfies $\mathrm{Sym}^{\mathrm{disc}}_j(m,cE)=c^2\,\mathrm{Sym}^{\mathrm{disc}}_j(m,E)$.
background
This module isolates the exact flat cross-term continuum symbol for 4D Regge calculus on the Freudenthal torus. At flat background, deficits vanish, so the Schläfli identity leaves the Hessian cross term $S''=\sum_h(dA_h)(d\delta_h)$. The binding object is that Hessian on plane-wave class strains with position-resolved deficit phasing (star-member cube offsets on t11; per-edge transported origins on t12/t13/t22).
The discrete exact Regge symbol packages the finite flat cross-term fold with a constant bookkeeping factor of 2 (the 3D ttSecondDifference parallel). The strain argument is a real $4\times 4$ matrix. The finite symbol already satisfies quadratic homogeneity under scalar multiplication of the strain; the discrete package inherits that scaling once the constant factor is unfolded.
Oracle verdict H_fold: the true Regge action Hessian annihilates vertex-gauge modes and sends normalized TT on the banked directions to $-1/4$. Distinct-hinge transported folds are not the continuum object.
proof idea
Short tactic proof. Unfold the discrete symbol to expose the constant bookkeeping factor times the finite exact Regge symbol. Rewrite the finite factor by the upstream homogeneity theorem finiteExactReggeSymbol_smul (itself an unfold-and-apply of the exact flat cross-term fold smul lemma on the real mode family). The remaining scalar identity $k\cdot(c^2 s)=c^2\cdot(k\cdot s)$ is closed by ring.
why it matters
Structural homogeneity lemma in the MODEL tier around exactFlatCrossTermFold / finiteExactReggeSymbol. Quadratic scaling in strain is the expected Hessian signature of a quadratic action cross term; without it, continuum-symbol Tendsto statements and m² certificates on the banked family (axisTTPlus, axisTTCross, decoyGauge) would not scale consistently under amplitude changes.
No downstream consumers are wired yet (used_by empty). It sits beside zero-momentum member-drop and status-flag lemmas as bookkeeping infrastructure for the H_fold pivot. Open items it supports but does not close: FoldAlongM2Tendsto / geometric ContinuumSymbolIs for all modes, ledger $S_{RS}$ inhabit, and e0 isotropy. ContinuumSymbolIs presently binds the bare finite sequence in Preflight, not a constant face. Does not address transported-gauge closure.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.