partialDeficitClassKernel_values
plain-language theorem explainer
At the flat Freudenthal seed hinge, the two-simplex partial deficit class kernel takes values −1/2, −1/2, and +1/2 on edge classes 3, 7, and 11. Anyone citing the support of ∂(2π−θ₀−θ₁)/∂ℓ² on the 15-class stencil would quote this packaging. The proof is a one-line conjunction of the three class-wise evaluations.
Claim. At the flat seed hinge, the two-simplex partial deficit class kernel $K:\{0,\ldots,14\}\to\mathbb{R}$ defined by $K(d)=\partial(2\pi-\theta_0-\theta_1)/\partial\ell^2_d$ satisfies $K(3)=-1/2$, $K(7)=-1/2$, and $K(11)=+1/2$.
background
This module sits in the QG full-theory campaign as the next kernel-checked increment after the flat 4D Regge hinge cosine kernel. Scope is the seed triangle hinge ${0,e_0,e_0+e_1}$ inside its two seed-cell Freudenthal 4-simplices only; the full lattice orbit sum remains open.
The local angle kernel at flat, obtained from the arccos chain factor $-1/\sin=-\sqrt{2}$ applied to the cosine derivatives, maps slots $(8,9)\mapsto(-1/4,1/2)$. Assembling those local slots through each seed simplex's localEdgeClass table yields a gradient of the two-simplex partial deficit $2\pi-\theta_0-\theta_1$ on the 15 global edge classes.
The definition partialDeficitClassKernel is exactly that assembly: sum of the two single-simplex deficit kernels over classes. Upstream theorems evaluate it at classes 3, 7, and 11 by unfolding the assembly and deciding the local-class equalities.
proof idea
One-line term proof: the conjunction of the three prior evaluations partialDeficitClassKernel_three, partialDeficitClassKernel_seven, and partialDeficitClassKernel_eleven. Each of those unfolds the assembly definition, rewrites with assembleClassKernel_eval, and decides which of the active local slots (8 and 9) land in the target class.
why it matters
This is the packaged form of deliverable A item 4 in the module: the two-simplex partial deficit gradient at flat is supported on classes $(3,7,11)$ with values $(-1/2,-1/2,+1/2)$. It closes the class-kernel half of the seed-hinge analysis after the cosine and angle kernels.
No downstream consumers are wired yet (used_by is empty). The result is still the natural citation point for any later Hessian or orbit-sum argument that needs the nonzero support of the partial deficit on the 15-class stencil. It does not complete the flat Hessian of the 4D Regge action, nor prove $S_{\mathrm{RS}}$ converges to Einstein–Hilbert in 4D, nor flip gap_action_recovery.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.