singleSimplexDeficitKernel_nine
plain-language theorem explainer
At the flat Freudenthal seed hinge, the single-simplex deficit gradient in squared-edge slot 9 equals -1/2. Anyone assembling two-simplex partial-deficit class kernels or star-member evaluations cites this slot value. The proof unfolds the per-simplex deficit definition (minus the angle kernel) and substitutes the known angle-kernel value 1/2 at slot 9.
Claim. At the flat seed hinge, the single-simplex contribution to the deficit gradient $\partial(-\theta)/\partial\ell^2$ in squared-edge coordinate $9$ equals $-1/2$.
background
This module sits in the QG full-theory campaign on the 4D Regge seed hinge ${0,e_0,e_0+e_1}$ inside its two seed-cell Freudenthal 4-simplices. Scope is deliberately local: only those two simplices, sharing one squared-edge vector; the full lattice orbit sum remains open. Prior work already gives the Gram-projection cosine of the dihedral angle, its flat value $\cos=1/\sqrt{2}$, and all ten coordinate derivatives of that cosine.
The angle kernel is the arccos-chain transport of those cosine derivatives: factor $-1/\sin=-\sqrt{2}$ at flat, so slots 8 and 9 map to $(-1/4,1/2)$ and slots 0–7 vanish. The single-simplex deficit kernel is defined as the negation of that angle kernel, because the deficit is $\delta=2\pi-\sum\theta$ and each simplex contributes $-\theta'$. Upstream, the angle kernel at slot 9 is already proved equal to $1/2$.
proof idea
Term-mode, three steps. Unfold the definition of the single-simplex deficit kernel (it is literally minus the angle kernel). Rewrite with the upstream evaluation that the angle kernel at index 9 equals $1/2$. Close by norm_num, which reduces $-1/2$ to the target literal.
why it matters
This is one of the two nonzero single-simplex deficit slots that feed the assembled two-simplex partial-deficit gradient on the 15 edge classes. Downstream, the class-kernel theorems for classes 3 and 7 both route through this value when they evaluate the local-edge-class table at slot 9; the star-kernel private lemmas member0_eval and member1_eval likewise rewrite through the same single-simplex kernel and land the $-1/2$ contributions on classes 7 and 3 respectively.
In the module deliverable list this is item 4 (angle and two-simplex partial deficit kernels). It does not touch the open full-orbit sum, the flat Hessian of the 4D Regge action, or the still-open claims S_RS_converges_EH_4d and gap_action_recovery. It is pure kernel arithmetic at the flat seed point.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.