exactDeficitDot
plain-language theorem explainer
Dispatches the linearized hinge deficit on plane-wave class strains by orbit type: type-(1,1) uses star-member cube offsets at the hinge base under the covering permutation; the remaining orbits use per-edge transported origins. Anyone assembling the flat Regge cross-term Hessian cites it as the dδ factor in Σ (dA)(dδ). The body is a pure match on HingeOrbitType.
Claim. For a hinge orbit type $\tau$, a $4\times 4$ strain matrix $H$, a wavevector $m\in\mathbb{R}^4$, and discrete hinge labels $(s,t)$, the exact deficit derivative is the real number obtained by: if $\tau=(1,1)$, the star-resolved phased deficit contraction at the hinge base under the orbit covering permutation; otherwise, the edge-origin phased deficit contraction for that orbit.
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 names that Hessian on plane-wave class strains with position-resolved deficit phasing, the binding object behind the oracle verdict $H_{\mathrm{fold}}$.
A hinge orbit type labels the combinatorial class of a 4D Freudenthal hinge (type $(1,1)$ versus $(1,2)$/complements and $(2,2)$). Mat4 is a real $4\times 4$ matrix (class strain); Wave4 is a real 4-vector (Bloch wavevector). The geometric deficit is the classical $2\pi-\sum\theta$ at a hinge.
Upstream, the type-$(1,1)$ branch is the resolved star sum: six star members, each pushed by a covering permutation and evaluated at the hinge base plus a cube-offset transport. Other orbits route through edge-origin phasing from the star-edge-origins analysis, which removes the gauge residue that plagued the distinct-hinge transported fold.
proof idea
Definition by case split on hinge orbit type. The $(1,1)$ arm applies the resolved star contraction at hingeBase s t with the type-$(1,1)$ covering permutation. Every other orbit arm is a direct call to the edge-origin phased deficit. No algebraic simplification; pure dispatch.
why it matters
This is the deficit half of the exact flat cross-term slot: the parent definition multiplies area-class contraction at the hinge base by this value (zero off-orbit). Homogeneity in the strain matrix is recorded immediately by the sibling scaling lemma, which cases on the same match.
In the Recognition gravity stack it is the MODEL-tier geometry for exactFlatCrossTermFold / finiteExactReggeSymbol, the continuum object that sends normalized TT on the banked directions to $-1/4$ and annihilates vertex-gauge modes. It does not yet elevate the nonlinear Regge action through Schläfli for every orbit, and the continuum Tendsto / ledger $S_{RS}$ inhabit questions remain open. It is the position-resolved replacement for the mis-transporting distinct-hinge fold.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.