singleSimplexDeficitKernel_le_seven
plain-language theorem explainer
For local edge slots 0 through 7 of the seed 4-simplex, the single-simplex deficit gradient vanishes at the flat Freudenthal point. Anyone assembling the two-simplex partial deficit kernel on the 15 edge classes cites this support restriction. The proof is a one-line simplification through the angle and cosine kernels, using that the cosine dihedral kernel is already zero on those slots.
Claim. For each local squared-edge coordinate index $k\in\{0,\ldots,9\}$ with $k\le 7$, the single-simplex contribution to the deficit gradient at the flat seed hinge is zero: if $\delta=2\pi-\sum\theta$ then the per-simplex term $-\theta'$ satisfies $\partial(-\theta)/\partial\ell_k^2=0$.
background
This module is the next kernel-checked increment in the 4D Regge seed-hinge campaign after 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.
The cosine dihedral kernel records all ten coordinate derivatives of $\cos$ of the seed-hinge dihedral angle at the flat Freudenthal point: slots 8 and 9 are nonzero ($\sqrt{2}/8$ and $-\sqrt{2}/4$), while slots 0 through 7 vanish. The angle kernel multiplies by the arccos chain factor $-1/\sin\theta=-\sqrt{2}$ at flat, so $\theta'=-(1/\sin\theta)\cdot\cos'$. The single-simplex deficit kernel is then $-\theta'$, the per-simplex contribution to $\partial(2\pi-\sum\theta)/\partial\ell^2$.
Upstream, the lemma that the cosine dihedral kernel is zero on indices with value at most 7 is already proved by exhaustive fin_cases. This declaration simply transports that support fact through the two linear rescalings.
proof idea
One-line simp proof. Unfold the single-simplex deficit kernel to $-$ the angle kernel, unfold the angle kernel to $-\sqrt{2}$ times the cosine dihedral kernel, and apply the upstream lemma that the cosine dihedral kernel vanishes for every $k$ with $k.\mathrm{val}\le 7$. The product is therefore zero. No case split is repeated here; the cases live in the cosine lemma.
why it matters
This is the support half of deliverable A item 4 in the module: the angle and two-simplex partial deficit kernels are carried only by the apex slots. Downstream, the assembly theorem that reduces the class-kernel sum over Fin 10 to the two active local slots (8 and 9) invokes exactly this vanishing on 0 through 7, so the 15-class stencil only sees classes hit by those two edges.
In the broader Recognition gravity stack this is a kernel-checked brick toward the flat Hessian of the 4D Regge action, not a completion of it. The module explicitly does not claim $S_{\mathrm{RS}}$ converges to Einstein-Hilbert in 4D, does not flip gap-action recovery, and does not reverse-engineer weights from EH. The result sits inside the seed-hinge, two-simplex fragment; the full orbit sum over all hinges is still open.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.