finiteExactReggeSymbol
plain-language theorem explainer
Names the exact-action continuum symbol sequence on the canonical 4-torus of side torusSide j: the bare Regge flat cross-term fold of a polarization matrix against the real Bloch mode. Gravity continuum-preflight and discrete-bookkeeping lemmas cite it as the frozen geometric target (before the factor-of-two package). The body is a one-line re-export of the definition in Regge4DExactActionSymbol.
Claim. For mesh index $j\in\mathbb{N}$, integer mode $m:\mathrm{Fin}\,4\to\mathbb{Z}$, and polarization matrix $E$, the finite exact Regge symbol is the real number given by the exact flat cross-term fold of $E$ against the real family mode at side $\mathrm{torusSide}(j)$. It is the bare $s''_{\mathrm{Regge}}$ face, prior to discrete bookkeeping.
background
This module freezes the independent continuum target, mesh carrier, TT data, pure-gauge family, and honesty decoys for the 4D Regge continuum campaign. Nothing here proves continuum recovery. The canonical carrier is a periodic Freudenthal 4-torus of side $N\ge 3$; polarizations are Frobenius-normalized Euclidean TT modes; the Einstein-Hilbert quadratic is frozen via kappa_einstein, not fitted from the lattice.
Upstream, the exact-action module defines the named continuum symbol sequence as the bare Regge cross-term: fold $E$ against the real mode family at mesh index $j$. That is the $s''{\mathrm{Regge}}$ face before discrete bookkeeping. The module doc marks this sequence (after oracle $H{\mathrm{fold}}$) as the named OPEN continuum target: $|k|^2$-normalized, to match the EH coefficient on TT and vanish on pure gauge. Legacy distinct-hinge folds are retained only for comparison.
proof idea
One-line abbrev re-export. No proof obligations: it aliases Regge4DExactActionSymbol.finiteExactReggeSymbol, whose body is exactFlatCrossTermFold E (familyRealMode j m). Local equality finiteExactReggeSymbol_eq is then rfl against the same fold at realMode (torusSide j) m.
why it matters
This is the frozen geometric continuum object for the QG full-theory 4D closure plan. Downstream, discreteExactReggeSymbol packages it as $2\cdot$ this symbol (3D-parallel bookkeeping); doubled_fold_is_the_named_object records that the doubled geometric object is exactly that package. Local preflight uses it in finiteExactReggeSymbol_eq and in face comparisons against the independently frozen EH TT coefficient (continuumEH_unitF_face_eq_frozen).
The ledger currently binds ContinuumSymbolIs to this bare sequence, not the doubled package. Open items remain: continuum Tendsto props, S_RS_converges_EH_4d uninhabited, and incomplete star-member offsets off the $t_{11}/t_{12}$ orbits. The design rule is observation, not fit: EH is frozen independently; later algebraic closers must match this symbol, never reverse-engineer lattice weights from the EH answer.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.