exactFlatCrossTermSlot
plain-language theorem explainer
Per-slot contribution to the exact flat Regge cross-term Hessian: when hinge slot (s,t) lies in orbit type ty, the value is the product of the phased area class-dot at the hinge base and the position-resolved deficit variation; otherwise zero. Gravity analysts assembling the continuum-facing fold cite it as the atomic summand. The body is a one-branch conditional definition, not a proved identity.
Claim. For a hinge orbit type $\mathrm{ty}$, a $4\times 4$ strain matrix $H$, a four-component wavevector $m$, and a hinge slot $(s,t)\in\{0,\ldots,23\}\times\{0,\ldots,9\}$, the exact flat cross-term slot equals the product of the phased class-dot of the slot orbit area covariance at the hinge base with the exact deficit variation whenever the slot belongs to orbit $\mathrm{ty}$, and equals $0$ otherwise.
background
At a flat Regge background all hinge deficits vanish, so the second variation of the action reduces by Schläfli to the pure cross term $S''=\sum_h (dA_h)(d\delta_h)$. This module builds that Hessian on plane-wave class strains with position-resolved deficit phasing: type-$(1,1)$ keeps star-member cube offsets, while the remaining orbit types use per-edge transported origins.
A slot is a pair $(s,t)$ indexing one of the $24\times 10$ hinge positions on the Freudenthal torus. The predicate isOrbit checks that the slot's classified hinge orbit equals the supplied type. The area factor is the phased class-dot of the transported slot-orbit area covariance against the strain $H$ and wave $m$ evaluated at the hinge base coordinate. The deficit factor is the orbit-type-resolved exact deficit variation (star-member phasing for t11; edge-origin transport for t12/t13/t22 and complements).
The ambient setting is the oracle-backed continuum symbol $H_{\mathrm{fold}}$: the true flat Hessian annihilates vertex-gauge modes and sends normalized TT on the banked directions to $-1/4$.
proof idea
Pure definition by cases. If the slot belongs to the given orbit type, return the product of two already-defined real quantities: the phased class-dot of the slot-orbit area covariance at the hinge base, and the exact deficit variation for that orbit type. Otherwise return zero. No lemmas are applied; the body is a single if on the decidable orbit membership predicate.
why it matters
This is the atomic summand of the continuum-facing flat cross-term. Downstream, exactFlatCrossTermOrbit sums it over all $24\times 10$ slots for a fixed orbit type, and the weighted fold of those orbits is the Hessian candidate after the $H_{\mathrm{fold}}$ oracle verdict. Homogeneity in the strain is discharged slotwise by exactFlatCrossTermSlot_smul (quadratic scaling $c^2$), then lifted to the full fold by exactFlatCrossTermFold_smul.
In the Recognition gravity stack this sits inside the MODEL tier for the geometry-derived flat cross-term (not yet Schläfli-elevated from the full nonlinear action for every orbit). It supports the banked TT certificates on symbolDir while leaving open the continuum tendsto statements (FoldAlongM2Tendsto, geometric ContinuumSymbolIs) and ledger recovery of $S_{RS}$.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.