exactFlatCrossTermFold
plain-language theorem explainer
Names the distinct-hinge weighted flat Regge cross-term on a 4×4 strain matrix and a 4-momentum wave: sum over hinge orbit types of star-size inverse times the orbit cross-term. Continuum-facing Hessian candidate after the H_fold oracle (TT modes to −1/4, gauge annihilated). Gravity analysts cite it as the bare s''_Regge face before bookkeeping. Definition is a weighted sum of per-orbit slot sums.
Claim. For a real $4\times 4$ strain matrix $H$ and wavevector $m\in\mathbb{R}^4$, the distinct-hinge weighted exact flat cross-term is $$\sum_{\tau}\, r_\tau^{-1}\, C_\tau(H,m),$$ where the sum runs over hinge orbit types $\tau$, $r_\tau$ is the geometric star size of type $\tau$ (6 for $(1,1)$-class, 4 for $(1,2)$-class, etc.), and $C_\tau$ is the double sum of position-resolved flat cross-term slots on that orbit.
background
At a flat Regge background all hinge deficits vanish, so the Schläfli identity reduces the second variation of the action to the pure cross term $S''=\sum_h (dA_h)(d\delta_h)$. This module fixes that Hessian on plane-wave class strains with position-resolved deficit phasing: type-$(1,1)$ keeps star-member cube offsets; the remaining orbit types use per-edge transported origins.
The oracle verdict $H_{\mathrm{fold}}$ (2026-07-21) states that the true continuum Hessian on the Freudenthal torus annihilates vertex-gauge modes and sends normalized TT on the banked directions to $-1/4$. The older distinct-hinge transported fold mis-transports and is retained only as legacy.
Upstream, exactFlatCrossTermOrbit sums the slot-level cross terms over the 24×10 star indexing for one orbit type; orbitStarSize supplies the geometric weights $r_\tau\in{4,6}$ from the star modules. $H$ here is the strain matrix, not the cost reparametrization $H(x)=J(x)+1$.
proof idea
Pure definition: unfold to a finite sum over HingeOrbitType, weighting each orbit contribution exactFlatCrossTermOrbit ty H m by the reciprocal star size (orbitStarSize ty)⁻¹. No tactics; the body is the weighted sum itself. Homogeneity and continuum-sequence equalities are proved later by unfolding this def and the orbit/slot layers.
why it matters
Binding continuum object of the exact-action symbol path. Downstream, finiteExactReggeSymbol is exactly this fold on the family real mode at torus side $N=j+3$; Preflight’s finiteExactReggeSymbol_eq is rfl against that. Structural lemmas (exactFlatCrossTermFold_smul, zero-momentum drops) and the status flag fold_retained_as_legacy_only (legacy Bloch fold ≠ this object) hang off it.
In the RS gravity stack this is the MODEL-tier bare $s''{\mathrm{Regge}}$ face used when comparing geometric fold to dictionary symbols and when packaging SRS→EH residuals. It does not yet close FoldAlongM2Tendsto / ContinuumSymbolIs for all modes, nor ledger $S{RS}$ / gap-action recovery; those remain open. It also does not flip the internal transported-gauge-zero certificate.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.