exactFlatCrossTermOrbit
plain-language theorem explainer
Sums the exact flat Regge cross-term over all 24 star slots and 10 tetra types for one hinge-orbit class, at a 4×4 strain and Bloch wavevector. Gravity analysts cite it as the per-orbit building block of the continuum-facing Hessian candidate after the H_fold oracle. The body is a plain double sum of the slotwise area×deficit products.
Claim. For a hinge-orbit type $\tau$, a real $4\times 4$ strain matrix $H$, and a wavevector $m\in\mathbb{R}^4$, define the orbit cross-term as $\sum_{s=0}^{23}\sum_{t=0}^{9}$ of the exact flat slot contribution: area at the hinge base times the position-resolved deficit derivative when $(s,t)$ lies in orbit $\tau$, and $0$ otherwise.
background
This module isolates the exact flat cross-term continuum symbol that the H_fold oracle identifies as the true Regge Hessian on the Freudenthal torus: at vanishing background deficits, Schläfli reduces the second variation to $S''=\sum_h (dA_h)(d\delta_h)$. Plane-wave class strains carry position-resolved deficit phasing (star-member cube offsets for type $(1,1)$; per-edge transported origins for the remaining orbits).
Mat4 is a real $4\times 4$ matrix (strain); Wave4 is a map $\mathrm{Fin},4\to\mathbb{R}$ (Bloch momentum). Hinge orbits under coordinate permutation fall into six lattice types. Each slot contribution multiplies the phased class area covector against $H$ and $m$ at the hinge base by the exact deficit derivative, gated by orbit membership.
The double index runs over the 24 star members and 10 tetrahedron types that tile the local hinge geometry.
proof idea
Definitional double sum: unfold to $\sum_{s:\mathrm{Fin},24}\sum_{t:\mathrm{Fin},10}$ of the slot map. No lemmas; each summand is the gated product (phased area covector dotted into strain and wave) times the exact deficit derivative, or zero off-orbit. Downstream homogeneity proofs unfold this sum and push scalar factors through the slots.
why it matters
Parent object of the distinct-hinge weighted fold: that fold averages this orbit sum by the inverse orbit-star size over all six hinge types, and is the continuum-facing Hessian candidate after H_fold (oracle: annihilates vertex-gauge modes; normalized TT on axisTTPlus/symbolDir maps to $-1/4$). The quadratic scaling theorem for the fold is proved by unfolding through this orbit sum and the slot smul lemma.
In the RS gravity stack this is MODEL-tier geometry for the flat cross-term, not yet Schläfli-elevated from the full nonlinear action on every orbit. It feeds the finite exact Regge symbol sequence and the continuum preflight Tendsto story. Open items remain: FoldAlongM2Tendsto / ContinuumSymbolIs for all modes, ledger $S_{RS}$ inhabit, and e0 isotropy. Does not address the mis-transporting distinct-hinge Bloch fold that carries t12/t13 gauge residue.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.