partialDeficitClassKernel_eleven
plain-language theorem explainer
At the flat Freudenthal seed hinge, the two-simplex partial deficit kernel on edge class 11 equals +1/2. Gravity analysts building the 4D Regge Hessian cite this as the unique positive support entry among the three nonzero classes (3, 7, 11). The proof unfolds the class assembly on the two seed simplices, retains only the slot-8 contributions (both map to class 11), and reduces via the single-simplex slot-8 value 1/4.
Claim. At the flat Freudenthal seed hinge, the two-simplex partial deficit class kernel evaluates to $1/2$ on edge class $11$: $\partial(2\pi-\theta_0-\theta_1)/\partial\ell^2_{11}=1/2$, where the kernel is the sum of the two seed-simplex assemblies of the single-simplex deficit gradient onto the 15 edge classes.
background
This module sits in the QG full-theory campaign, one kernel-checked step past the flat 4D Regge hinge layer. Scope is the seed triangle hinge ${0,e_0,e_0+e_1}$ inside its two seed-cell Freudenthal 4-simplices only (permutations beginning $(0,1,\ldots)$); both share the same local squared-edge vector.
The geometric deficit at a hinge is $2\pi-\sum\theta$ (DihedralAngle/Schlaefli). Differentiating the two-simplex partial deficit $2\pi-\theta_0-\theta_1$ at flat, after the arccos chain factor $-1/\sin=-\sqrt{2}$, yields a single-simplex angle/deficit kernel supported on local slots 8 and 9. The class kernel packages those slot values onto the 15 global edge classes via each simplex's localEdgeClass table:
$$\mathrm{partialDeficitClassKernel}(d)=\mathrm{assemble}_0(d)+\mathrm{assemble}_1(d).$$
Upstream, assembleClassKernel_eval collapses each assembly to the two active slots, and singleSimplexDeficitKernel_eight gives slot 8 the value $1/4$.
proof idea
Term-mode arithmetic after unfolding. Unfold partialDeficitClassKernel to the sum of two assemblies. Rewrite each by assembleClassKernel_eval, leaving only the slot-8/9 conditionals. Four decide facts pin the class table: both seed simplices send local slot 8 to class 11 and slot 9 elsewhere, so each assembly contributes exactly singleSimplexDeficitKernel 8. Rewrite that by singleSimplexDeficitKernel_eight ($=1/4$) and finish with norm_num: $1/4+1/4=1/2$.
why it matters
Closes the class-11 entry of deliverable A item 4 in the module: the two-simplex partial deficit gradient $\partial(2\pi-\theta_0-\theta_1)/\partial\ell^2$ is supported on classes $(3,7,11)$ with values $(-1/2,-1/2,+1/2)$. Downstream, partialDeficitClassKernel_values packages this theorem with the class-3 and class-7 siblings into a single conjunction.
In the broader RS gravity program this is a concrete, transcendental-free kernel check on the seed hinge before any lattice orbit sum. It does not yet touch the flat Hessian of the full 4D Regge action, nor S_RS_converges_EH_4d, nor gap_action_recovery. Those remain open; this lemma only certifies one nonzero class value on the two-simplex seed.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.