singleSimplexDeficitKernel
plain-language theorem explainer
One seed 4-simplex's contribution to the Regge deficit gradient at the flat Freudenthal point: for each of the ten local squared-edge slots, the per-simplex term is minus the dihedral-angle derivative. Anyone building the two-simplex partial deficit or the star-local deficit kernel cites this packing. It is a one-line sign flip of the angle kernel (itself the arccos chain rule on the cosine kernel).
Claim. For each local squared-edge index $k \in \{0,\ldots,9\}$, the single-simplex deficit kernel equals $-\theta'_k$, where $\theta'$ is the flat dihedral-angle derivative obtained from the arccos chain rule on the cosine kernel. This is one seed simplex's contribution to $\partial\delta/\partial\ell^2$ with deficit $\delta = 2\pi - \sum\theta$.
background
The module sits in the QG full-theory campaign, one kernel-checked step past the flat 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.
Regge curvature lives in hinge deficits $\delta = 2\pi - \sum\theta$, so the gradient of the action needs $\partial\theta/\partial\ell^2$ at each simplex. The upstream angle kernel packages that derivative at flat: $\theta' = -(1/\sin\theta),\cos'$ with $1/\sin\theta = \sqrt{2}$, i.e. $\theta'_k = -\sqrt{2},(\cos\text{ kernel})_k$. The cosine kernel itself is supported only on local slots 8 and 9 (values $\sqrt{2}/8$ and $-\sqrt{2}/4$).
Negating the angle kernel converts $\theta'$ into the per-simplex piece of $\partial\delta/\partial\ell^2$. Assembling two such pieces (the two seed simplices sharing the hinge) yields the partial deficit class kernel on the 15 edge classes.
proof idea
Pure definition: one-line negation of the angle kernel. No tactics. Downstream evaluation lemmas (_eight, _nine, _le_seven) then unfold this def, rewrite the corresponding angle-kernel slot facts, and finish by norm_num or the cosine-kernel vanishing on slots $0$–$7$.
why it matters
This is the packing step between the angle kernel and every class-level deficit object in the module. partialDeficitClassKernel sums two assemblies of it (simplices 0 and 1); assembleClassKernel_eval proves that assembly collapses to the two active local slots. Evaluation theorems pin the concrete values: slot 8 maps to $+1/4$, slot 9 to $-1/2$, slots $0$–$7$ to $0$.
The star-kernel layer reuses it directly: member0_eval / member1_eval and starLocalDeficitKernel change into assemblies of this kernel, so the star-local deficit gradient inherits the same support and values. Module deliverable A lists exactly this chain: cosine derivatives, then angle kernel via $-1/\sin$, then per-simplex deficit contribution, then two-simplex partial deficit on classes $(3,7,11)$ with values $(-1/2,-1/2,+1/2)$.
It does not close the flat Hessian of the 4D Regge action, nor S_RS_converges_EH_4d, nor gap_action_recovery. Those remain open campaign targets.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.