deficitKernel12_dot_decoyTrace
plain-language theorem explainer
The type-(1,2) full-star deficit class kernel is orthogonal to the pure-trace decoy mode under the edge-class coefficient pairing. Analysts assembling the zero-momentum 4D Regge Hessian cite this to show true orbit weights kill pure gauge (the weight-1 provisional stencil did not). The proof rewrites the pairing as the committed full-star directional form on Hamming class weights and applies homothety stationarity.
Claim. The edge-class coefficient pairing of the type-$(1,2)$ full-star deficit kernel $K^{(1,2)}$ with the pure-trace decoy matrix $H_{\mathrm{tr}}$ vanishes: $\sum_{d\in\mathrm{Fin}\,15} K^{(1,2)}_d\,c_d(H_{\mathrm{tr}})=0$, where $c_d(H)=D^{\mathsf T}HD$ is the class load.
background
This module assembles the committed per-orbit star deficit kernels with Heron area gradients into the flat second-variation class quadratic of the 4D Regge action, at zero momentum only (constant edge-class perturbations). Edge classes are the 15 nonzero difference masks on the 4-cube; each class $d$ has a Hamming weight classWeightNat and a displacement vector whose squared length equals that weight.
The class coefficient of a $4\times 4$ matrix $H$ on class $d$ is the edge load $c_d(H)=D^{\mathsf T}HD$. For the pure-trace decoy $H_{\mathrm{tr}}=I$, this collapses to $c_d(H_{\mathrm{tr}})=|D|^2$, hence to the class weight. The type-$(1,2)$ full-star class kernel is the committed star deficit stencil for the $(1,2)$ hinge orbit; classDot is the plain $\mathbb{R}^{15}$ pairing of that kernel against class coefficients of a test matrix.
Upstream, classCoeff_decoyTrace and classDispSq_eq_weight identify the decoy coefficients with weights, and the hinge-kernel module supplies fullStar_homothety_stationary: the directional evaluation of the full-star kernel on the weight vector is zero.
proof idea
First prove pointwise that the class coefficients of the pure-trace decoy equal the realified Hamming weights, by rewriting through classCoeff_decoyTrace and classDispSq_eq_weight. Unfold the class pairing into an explicit sum over Fin 15. Commute factors in each summand so the sum matches the committed full-star directional form applied to the weight vector. Finish by invoking ReggeHinge4DStarKernel12.fullStar_homothety_stationary, which states that directional evaluation is zero.
why it matters
Deliverable A of the flat Hessian assembly requires that true-weight evaluations on axisTTPlus, decoyGauge, and decoyTrace all vanish; provisional weight-1 gave a nonzero $32$ on the same decoy. This lemma discharges the type-$(1,2)$ decoy-trace slot.
It is reused verbatim as deficitKernel12_dot_homothety (homothety alias of the same pairing) and as the t12 branch of orbitDeficit_dot_decoyTrace, which unifies the six $S_4$ orbit types. Together those feed the zero-momentum true-weight Hessian and the claim that true weights kill pure gauge at zero momentum.
Scope remains the QG full-theory campaign's per-cell Hessian; finite-momentum Bloch folding and the EH continuum limit (S_RS_converges_EH_4d, gap_action_recovery) stay open. No reverse-engineering from Einstein–Hilbert: kernels and counts come from committed geometry modules.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.