finiteExactReggeSymbol_eq
plain-language theorem explainer
On the side-$N$ Freudenthal 4-torus, the finite exact-action Regge continuum symbol at integer mode $m$ equals the flat cross-term fold of the polarization matrix at the corresponding real wave covector $k=2\pi m/N$. Anyone comparing discrete Regge symbols to the frozen weak-field EH target cites this identity. The proof is pure definitional equality (`rfl`).
Claim. For every $j\in\mathbb{N}$, integer mode $m:\mathrm{Fin}\,4\to\mathbb{Z}$, and real $4\times 4$ matrix $E$, the finite exact Regge continuum symbol at side $N=\mathrm{torusSide}(j)$ and mode $m$ equals the exact flat cross-term fold of $E$ evaluated at the real wave covector $k=2\pi m/N$.
background
This module is the first binding increment of the 4D continuum closure plan for Regge gravity. It freezes the independent continuum target, canonical mesh, normalized TT data, pure-gauge family, and honesty decoys before any continuum-limit proof. Nothing here claims continuum recovery of Einstein-Hilbert.
The carrier is the canonical periodic Freudenthal 4-torus of side $N\ge 3$. Integer modes IntMode4 are commensurate wave vectors $m:\mathrm{Fin},4\to\mathbb{Z}$; realMode N m produces the real covector $k=2\pi m/N$. Polarizations are real $4\times 4$ matrices (Mat4).
The continuum object named in the frozen contract is the exact-action symbol built from exactFlatCrossTermFold (re-exported here as the finite exact Regge symbol on side torusSide j). Legacy distinct-hinge and bare Bloch folds are retained only for comparison and are not the continuum target.
proof idea
One-line definitional proof: rfl. In this module finiteExactReggeSymbol is an abbrev re-export of Regge4DExactActionSymbol.finiteExactReggeSymbol, and exactFlatCrossTermFold is the matching abbrev of the flat cross-term fold. Unfolding both sides yields identical terms at realMode (torusSide j) m, so Lean closes by reflexivity with no lemmas or tactics.
why it matters
The module doc freezes the OPEN continuum target as: the exact flat cross-term symbol finiteExactReggeSymbol, $|k|^2$-normalized, should equal the independently frozen EH coefficient on TT polarizations and vanish on pure gauge. This theorem pins that symbol, by definition, to the flat cross-term fold at the real mode of the side-$N$ torus.
It is bookkeeping for the QG full-theory campaign rather than a continuum theorem: S_RS_converges_EH_4d remains uninhabited, and gapActionRecovery is false. No downstream users are recorded yet; the identity exists so later Tendsto and residual comparisons can quote a single named continuum face without re-deriving the fold. It does not reverse-engineer lattice weights from the EH answer: the EH quadratic stays frozen independently of the lattice symbol.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.