partialDeficitClassKernel_three
plain-language theorem explainer
At the flat Freudenthal seed hinge, the two-simplex partial deficit gradient on edge class 3 equals -1/2. Gravity analysts building the 4D Regge Hessian cite this as one of the three nonzero support values on the 15-class stencil. The proof unfolds class assembly on the two seed simplices, kills three inactive local-edge matches by decision, and reduces the surviving slot-9 term via the single-simplex deficit kernel.
Claim. At the flat seed-hinge configuration, the two-simplex partial deficit class kernel on edge class $3$ equals $-1/2$: $$\frac{\partial}{\partial \ell^2_{\mathrm{class}\,3}}(2\pi - \theta_0 - \theta_1) = -\tfrac12.$$
background
The module treats the seed triangle hinge ${0,e_0,e_0+e_1}$ inside its two seed-cell Freudenthal 4-simplices (permutations beginning $(0,1,\ldots)$). Deliverable A builds the dihedral cosine of that hinge as a Gram-projection function of the ten local squared edge lengths, evaluates it at the flat point ($\cos=1/\sqrt{2}$), and differentiates. The local angle kernel then follows from the arccos chain factor $-1/\sin=-\sqrt{2}$ at flat.
The two-simplex partial deficit is $2\pi-\theta_0-\theta_1$. Its class kernel sums, over the two seed simplices, an assembly of the single-simplex deficit kernel through the local edge-class table (15 classes). The assembly evaluation lemma reduces each simplex contribution to the two active apex slots 8 and 9 only: a class $d$ receives the slot-8 (resp. slot-9) kernel value precisely when that slot's local edge class equals $d$, else zero.
The single-simplex deficit kernel at slot 9 is already known to equal $-1/2$, from the angle kernel at that slot.
proof idea
Unfold the partial deficit class kernel as the sum of assemblies on seed simplices 0 and 1. Rewrite each assembly by the evaluation lemma, leaving four conditional terms (slots 8 and 9 on each of the two simplices). Decide the four local-edge-class equalities against class 3: three are false and drop; only simplex 1 at slot 9 matches. Substitute the single-simplex deficit kernel identity at slot 9 ($=-1/2$) and close by numeric normalization.
why it matters
This pins one of the three nonzero support values of the two-simplex partial deficit gradient at flat. The packaging theorem records the full support: classes $(3,7,11)$ with values $(-1/2,-1/2,+1/2)$. The hinge-fixing axis-swap symmetry theorem uses the class-3 value directly (the swap sends class 3 to class 7 and must preserve the kernel).
In the QG full-theory campaign this is item 4 of deliverable A in the Regge hinge dihedral kernel module: kernel-checked partial deficit gradients on the 15-class stencil, after the flat cosine and its ten coordinate derivatives. Module scope is explicit that the full lattice orbit sum over all hinges remains open, and that this 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.