singleSimplexDeficitKernel_eight
plain-language theorem explainer
At the flat Freudenthal seed, one seed 4-simplex contributes +1/4 to the deficit gradient in squared-edge slot 8. Anyone assembling two-simplex partial-deficit or star-member class kernels cites this slot evaluation. The proof unfolds the definition as the negated angle kernel and rewrites by the already-proved slot-8 angle value.
Claim. At the flat seed configuration, the single seed-simplex contribution to the deficit-angle gradient with respect to local squared edge length slot $8$ equals $\frac{1}{4}$.
background
In 4D Regge calculus, curvature sits on triangular hinges as angle deficits $\delta = 2\pi - \sum \theta$, with each $\theta$ a dihedral angle between 4-simplices meeting at the hinge. This module treats only the seed hinge ${0, e_0, e_0+e_1}$ inside its two seed-cell Freudenthal 4-simplices, parameterized by the ten local squared edge lengths, and never redefines the Freudenthal incidence or 15-class stencil APIs.
The angle kernel is $\partial\theta/\partial\ell^2_k$ at flat for each local edge slot $k\in\mathrm{Fin},10$. The single-simplex deficit kernel is defined by negating that angle kernel, since each simplex contributes $-\theta'$ to $\partial\delta/\partial\ell^2$. Upstream, the angle kernel at slot 8 equals $-1/4$, obtained from the arccos chain factor $-\sqrt{2}$ times the cosine-derivative value $\sqrt{2}/8$ at the flat point where $\cos\theta=1/\sqrt{2}$.
proof idea
One short tactic proof. Unfold the single-simplex deficit kernel definition (negation of the angle kernel). Rewrite by the upstream theorem that the angle kernel at slot 8 equals $-1/4$. Finish with norm_num to obtain $+1/4$.
why it matters
Slot 8 is one of the two nonzero support slots of the local angle kernel (with slot 9). Its single-simplex deficit value is the concrete input that class-assembly maps into the 15 edge-class partial-deficit gradient, and that the two seed-star member evaluations reuse when they rewrite through the same assembly.
Downstream, the class-11 partial-deficit evaluation and the private star-member evaluations for the two seed simplices all depend on this number. In the QG full-theory campaign this is a kernel-checked increment after the flat cosine and angle kernels: it advances deliverable A (angle and two-simplex partial deficit kernels) without closing the full lattice orbit sum, the flat Hessian of the 4D Regge action, or RS-to-Einstein-Hilbert recovery.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.