finiteExactReggeSymbol
plain-language theorem explainer
Names the bare continuum Regge symbol sequence s''_Regge(j,m;E): the exact flat cross-term Hessian evaluated on the plane-wave family of side N=j+3 with integer mode m and strain matrix E. Gravity analysts cite it as the H_fold continuum face before the discrete factor-2 bookkeeping. The body is a one-line application of the distinct-hinge weighted fold to the real Bloch mode.
Claim. For each resolution index $j\in\mathbb{N}$, integer wavevector $m\in\mathbb{Z}^4$, and strain matrix $E\in M_4(\mathbb{R})$, the finite exact Regge symbol is the real number obtained by evaluating the distinct-hinge weighted flat cross-term fold of $E$ on the real plane-wave mode with components $2\pi m_i/(j+3)$.
background
In 4D Regge calculus on the Freudenthal torus, the second variation of the action at a flat background reduces (by Schläfli) to the pure cross term $S''=\sum_h (dA_h)(d\delta_h)$, since background deficits vanish. The module isolates that Hessian on plane-wave class strains with position-resolved deficit phasing: star-member cube offsets for the $t_{11}$ orbit and per-edge transported origins for the remaining hinge orbits.
The binding continuum-facing object is the distinct-hinge weighted fold, which averages each hinge-orbit contribution by the inverse star size. Oracle verdict $H_{\mathrm{fold}}$ asserts that this true Hessian annihilates vertex-gauge modes and sends normalized TT polarizations on the symbol direction to $-1/4$. The older all-orbit Bloch fold is explicitly not the continuum object (gauge residue on $t_{12}/t_{13}$).
The continuum family uses side length $N=j+3$, matching the preflight torus side. The real mode attached to integer $m$ is the standard Bloch wave $k_i=2\pi m_i/N$. Strain matrices are plain $4\times 4$ real matrices.
proof idea
Pure definitional wrapper: feed the strain matrix $E$ and the family real mode of $(j,m)$ into the already-defined distinct-hinge weighted flat cross-term fold. No tactics, no lemmas beyond the two callees. The equality to the fold at realMode (torusSide j) m is later recorded by rfl in the preflight re-export.
why it matters
This is the MODEL-tier continuum face that ContinuumSymbolIs binds to in the preflight layer: the $|k|^2$-normalized Tendsto target is the sequence of these bare symbols, not a constant face and not the doubled package. Downstream, the discrete exact Regge symbol is defined as the 3D-parallel bookkeeping package $2\cdot$ this object; doubled_fold_is_the_named_object and discreteExactReggeSymbol_eq make that factor explicit.
It sits inside the gravity analysis chain that aims to recover the Einstein-Hilbert TT coefficient from the Regge Hessian on the Freudenthal lattice (D=3 spatial plus time, eight-tick compatible discretization). Open items flagged by the module remain: geometric Tendsto for all modes (FoldAlongM2Tendsto), ledger $S_{RS}$ inhabit, and $e_0$ isotropy. The definition does not itself close those; it only names the sequence they must converge to.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.