orbitDeficit_dot_decoyTrace
plain-language theorem explainer
For every S₄ hinge-orbit type, the star deficit kernel is orthogonal to the pure-trace decoy (the Euclidean identity) under the edge-class pairing. Gravity analysts cite this when checking that true-weight zero-momentum Hessians kill pure gauge/trace modes. The proof is a six-way case split that reuses the four committed kernel-dot-decoy lemmas, with (2,1) and (3,1) reduced by complement transport.
Claim. For every hinge-orbit type $\tau$ among the six $S_4$ classes, the class pairing of the corresponding star deficit kernel with the pure-trace decoy $H=I$ vanishes: $\langle K_\tau,\,\mathrm{class}(I)\rangle=0$.
background
This module assembles the flat second-variation class quadratic of the 4D Regge action at zero momentum: orbit-count-weighted sums of $(dA\cdot c)(d\delta\cdot c)$ over the six $S_4$ hinge types, with committed counts $72/48/48/24/24/24$. Scope is per-cell Hessian only; finite-momentum Bloch folding remains open.
The pure-trace decoy is the Euclidean identity matrix (not transverse-traceless). The class pairing classDot contracts a $\mathrm{Fin},15\to\mathbb{R}$ kernel against the fifteen edge-class coefficients of a symmetric $4\times4$ perturbation. Each orbit type has a committed star deficit kernel; types $(2,1)$ and $(3,1)$ equal the $(1,2)$ and $(1,3)$ kernels on edge classes because vertex complement $m\mapsto m\oplus 15$ preserves difference masks.
Upstream, the four representative kernels already satisfy the same vanishing: each deficitKernel**_dot_decoyTrace proves the pairing is zero by identifying class coefficients of the identity with class weights and using committed homothety stationarity.
proof idea
Case-split on the six constructors of HingeOrbitType. For t11, t12, t13, and t22, apply the matching upstream lemma (deficitKernel11/12/13/22_dot_decoyTrace) directly. For t21, rewrite the orbit kernel via kernel21 (complement transport identity) and reuse the type-$(1,2)$ lemma; likewise t31 rewrites through kernel31 to the type-$(1,3)$ lemma. No new arithmetic: pure dispatch plus the two transport equalities.
why it matters
Deliverable A of the Regge flat Hessian assembly requires that true weights kill pure gauge and pure trace at zero momentum (provisional weight-1 left a nonzero residue $32$ on the same decoy). This lemma is the per-orbit deficit half of that check: the downstream theorem trueWeightZeroMomQuadratic_decoyTrace unfolds the orbit-sum quadratic and invokes orbitQuadratic_of_deficit_zero with exactly this vanishing for every type, concluding the full true-weight quadratic is zero on the identity.
It sits inside the QG full-theory campaign toward continuum Einstein–Hilbert recovery, but does not itself prove $S_{\mathrm{RS}}$ converges to EH in 4D, nor flip gap_action_recovery. The geometric inputs (orbit counts, area gradients, deficit kernels) come from committed modules rather than reverse-engineered continuum weights.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.