deficitKernel13_dot_decoyTrace
plain-language theorem explainer
The type-(1,3) full-star deficit class kernel is orthogonal to the pure-trace (homothety) decoy mode in the 15-dimensional edge-class space. Anyone assembling the zero-momentum 4D Regge Hessian cites this to show true weights kill the conformal decoy. The proof rewrites the class coefficient of the decoy as Hamming weight and invokes the committed full-star homothety-stationarity identity.
Claim. The class-space pairing of the committed type-$(1,3)$ full-star deficit kernel with the pure-trace decoy matrix vanishes: $\langle K^{(1,3)},\, H_{\mathrm{tr}}\rangle_{\mathrm{class}}=0$. Equivalently, after identifying class coefficients of $H_{\mathrm{tr}}$ with Hamming weights of the 15 nonzero edge masks, the weighted directional sum of the kernel against those weights is zero.
background
This module assembles the zero-momentum per-cell Hessian of the 4D Regge action from committed star deficit kernels and Heron area gradients, replacing the provisional weight-1 aggregate. Scope is constant edge-class perturbations only; finite-momentum Bloch folding remains open.
Edge classes are the 15 nonzero difference masks on the 4-cube. The class coefficient of a symmetric $4\times 4$ matrix $H$ on class $d$ is $c_d(H)=D^\top H D$ (edge load). The decoy trace mode is the identity: its class coefficients equal squared displacements, which coincide with the natural Hamming weights of the masks. The type-$(1,3)$ full-star class kernel is the committed orbit-summed deficit response on those 15 classes.
The class pairing classDot is the ordinary sum of kernel values times class coefficients. Upstream, classCoeff_decoyTrace and classDispSq_eq_weight identify the decoy's coefficients with those weights; the kernel module supplies stationarity of the full star under pure homothety.
proof idea
First prove pointwise that the class coefficient of the decoy equals the real Hamming weight: rewrite via classCoeff_decoyTrace then classDispSq_eq_weight, and funext.
Unfold the class pairing to a finite sum over Fin 15. Commute factors (mul_comm) so the sum is exactly the full-star directional evaluation of the weight function. That evaluation is zero by the committed lemma fullStar_homothety_stationary on the type-$(1,3)$ kernel.
why it matters
Deliverable A of the flat Hessian assembly requires that true-weight kernels kill pure gauge and pure trace at zero momentum (provisional weight-1 left a nonzero residue 32 on the same decoy). This lemma discharges the type-$(1,3)$ trace channel.
Downstream, deficitKernel13_dot_homothety is the same statement under the homothety name, and orbitDeficit_dot_decoyTrace cases over all six $S_4$ hinge orbit types, routing the $(1,3)$ arm here. Together with the sibling kernel dots, it feeds the zero evaluations of the assembled quadratic on decoyTrace.
In the broader QG campaign this is local Hessian hygiene, not continuum recovery: the module explicitly does not prove $S_{\mathrm{RS}}\to\mathrm{EH}_{4d}$ and does not flip gap_action_recovery. Finite-momentum phase folding across hinge translates remains open.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.