partialDeficitClassKernel_zero_off
plain-language theorem explainer
The two-simplex partial deficit class kernel vanishes on every edge class except 3, 7, and 11. Anyone tracking flat Hessian support of the seed-hinge Regge deficit cites this support lemma. The proof evaluates the assembly on the two seed simplices, reads the four active local-edge classes by decision, and kills the remaining branches.
Claim. For every edge class $d \in \{0,\ldots,14\}$, if $d \notin \{3,7,11\}$, then the two-simplex partial deficit class kernel at the flat Freudenthal point satisfies $\partial(2\pi-\theta_0-\theta_1)/\partial\ell^2_d = 0$.
background
This module is the next kernel-checked increment in the 4D Regge seed-hinge campaign after the flat cosine kernel. Scope is the seed triangle hinge inside its two seed-cell Freudenthal 4-simplices only; the full lattice orbit sum remains open.
The partial deficit class kernel is the flat gradient $\partial(2\pi-\theta_0-\theta_1)/\partial\ell^2$ assembled onto the 15 global edge classes. It sums the single-simplex deficit kernels of the two seed simplices after pushing local slots through the incidence map localEdgeClass.
Assembly reduces to the two active local slots (8 and 9): for each simplex $s$ and class $d$, the assembled value is the sum of the slot-8 and slot-9 single-simplex kernels gated by whether those slots land in class $d$. Only those gates can be nonzero.
proof idea
Unfold the partial deficit class kernel into the sum of two assemblies. Apply the assembly-evaluation lemma twice so each term becomes a pair of if-gated single-simplex kernels on slots 8 and 9. Decide the four local-edge-class identities: simplex 0 maps slots 8,9 to classes 11,7; simplex 1 maps them to 11,3. Under the hypotheses $d\neq 3,7,11$, every gate is false, so each if-branch is zero; norm_num closes.
why it matters
Module deliverable A states that the two-simplex partial deficit gradient is supported exactly on classes $(3,7,11)$ with values $(-1/2,-1/2,+1/2)$. This theorem is the vanishing half of that support claim: off those three classes the kernel is identically zero.
Downstream, the hinge-fixing symmetry theorem uses the vanishing (together with the explicit nonzero values on 3 and 7) to prove invariance under the incidence-layer axis swap $2\leftrightarrow 3$. That symmetry is part of the nonvacuity/symmetry/decoy package for the seed-hinge kernel.
In the broader QG campaign this is a local flat-kernel fact only. It does not complete the flat Hessian of the 4D Regge action, does not prove continuum recovery of Einstein–Hilbert, and does not close the full orbit sum over hinges.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.