orbitDeficitKernel
plain-language theorem explainer
Dispatch table sending each of the six S₄ hinge orbit types to its committed star-class deficit kernel on the 15 edge classes. Gravity analysts cite it when assembling zero-momentum Regge Hessians or Bloch orbit folds. The body is pure pattern-match: (2,1) and (3,1) reuse the (1,2) and (1,3) kernels by identity transport under vertex complement.
Claim. For each lattice hinge orbit type $\tau\in\{t_{11},t_{12},t_{21},t_{13},t_{31},t_{22}\}$, the orbit deficit kernel is the map $K_\tau:\mathrm{Fin}\,15\to\mathbb{R}$ equal to the committed full-star class kernel of that type; types $(2,1)$ and $(3,1)$ are identified with the committed $(1,2)$ and $(1,3)$ kernels by identity transport on edge classes.
background
The module assembles the flat second-variation class quadratic of the 4D Regge action at zero momentum. Hinges fall into six $S_4$ orbit types under coordinate permutation. Each type has a committed star-class deficit kernel: a real vector on the 15 edge-difference classes recording how a constant edge-class perturbation sources deficit at a hinge star.
Vertex complement $m\mapsto m\oplus 15$ preserves difference masks, so edge-class indices are invariant. Consequently the type-$(2,1)$ kernel equals the committed type-$(1,2)$ kernel, and type-$(3,1)$ equals type-$(1,3)$. Those equalities are packaged as the local aliases used here.
The six kernels (with explicit entries involving $\pm 1$, $\pm\sqrt{2}/2$, $\pm\sqrt{3}$, etc.) are the geometric inputs that later pair with Heron area covectors to form the true-weight Hessian terms $(dA\cdot c)(d\delta\cdot c)$.
proof idea
Definition by exhaustive case split on HingeOrbitType. Types $t_{11}$, $t_{12}$, $t_{13}$, $t_{22}$ point directly at the corresponding imported fullStarClassKernel. Types $t_{21}$ and $t_{31}$ point at the local aliases that are definitionally the $(1,2)$ and $(1,3)$ kernels. No computation; pure routing.
why it matters
This is the single entry point that every per-orbit deficit contraction uses. Downstream, fullMomentOrbitContribution_of_deficit_zero kills an orbit contribution once the class-dot of this kernel vanishes; factorizedOrbitSlotTerm multiplies the phased area covector by the phased deficit kernel; factorizedBlochFoldOrbit_zeroMomentum recovers the committed zero-momentum quadratic from the Bloch fold; and complement_orbit_deficit_kernels records the $(2,1)\leftrightarrow(1,2)$ and $(3,1)\leftrightarrow(1,3)$ equalities as rfl.
In the QG campaign it replaces provisional weight-1 aggregates by geometry-committed kernels, enabling the true-weight Hessian that kills pure gauge at zero momentum. Finite-momentum Bloch phase folding across hinge translates remains open; this definition does not close $S_{\mathrm{RS}}\to\mathrm{EH}_{4d}$ or flip gap-action recovery.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.