orbitQuadratic_of_deficit_zero
plain-language theorem explainer
If the edge-class deficit kernel of a hinge orbit type is orthogonal to a constant edge-class perturbation, the zero-momentum orbit quadratic for that type vanishes. Gravity analysts assembling the true-weight 4D Regge Hessian cite this when killing pure-gauge and decoy modes. The proof is a one-line unfold: the quadratic is a product whose second factor is that class-dot, so mul_zero finishes it.
Claim. Let $\mathrm{ty}$ be one of the six $S_4$ hinge orbit types and let $H$ be a $4\times 4$ edge-class matrix. If the class-dot of the committed star deficit kernel for $\mathrm{ty}$ against $H$ is zero, then the zero-momentum orbit quadratic of $\mathrm{ty}$ on $H$ is zero.
background
This module assembles the flat second-variation class quadratic of the 4D Regge action at zero momentum. Committed per-orbit star deficit kernels (types $(1,1)$, $(1,2)$, $(2,1)$, $(1,3)$, $(3,1)$, and the remaining $S_4$ class) are paired with Heron area gradients; the true-weight Hessian is the orbit-count-weighted sum of products $(dA\cdot c)(d\delta\cdot c)$ with counts $72/48/48/24/24/24$.
The class-dot is the pairing of a $\mathrm{Fin},15\to\mathbb{R}$ kernel against the fifteen edge-class coefficients of a matrix $H$. The orbit deficit kernel dispatches on hinge orbit type to the committed full-star class kernels (with $(2,1)$ and $(3,1)$ identified to $(1,2)$ and $(1,3)$ by complement transport on edge classes). The zero-momentum orbit quadratic for a single type is the product of the area-gradient class-dot and the deficit-kernel class-dot.
Scope is strictly constant (zero-momentum) edge-class perturbations per cell. Finite-momentum Bloch folding remains open, and the assembly does not claim Einstein–Hilbert recovery or action-gap closure.
proof idea
One-line wrapper. Unfold the definition of the zero-momentum orbit quadratic (a product whose second factor is the class-dot of the orbit deficit kernel against $H$). Rewrite that factor by the hypothesis that it equals zero, then apply mul_zero.
why it matters
This lemma is the per-orbit vanishing step used by the three deliverable evaluations of the true-weight zero-momentum Hessian: it vanishes on axisTTPlus, on the pure-gauge decoy, and on the trace decoy. Each parent theorem sums over orbit types and invokes this lemma once the corresponding deficit-kernel class-dot has been shown to be zero.
In the QG full-theory campaign this is the algebraic reason true weights kill pure gauge at zero momentum (the provisional weight-1 aggregate gave a nonzero $32$ on the same decoy). It sits inside deliverable A of the Regge flat Hessian assembly and does not touch the open finite-momentum Bloch problem or the still-open $S_{\mathrm{RS}}\to\mathrm{EH}_{4d}$ convergence claim.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.