partialDeficitClassKernel
plain-language theorem explainer
Defines the two-simplex partial deficit gradient on the 15 edge classes at the flat Freudenthal seed hinge: the sum of the two seed-simplex assemblies of the local angle-kernel contribution. Anyone computing the flat Regge deficit stencil in 4D cites it. The body is a two-term sum of assembleClassKernel applied to singleSimplexDeficitKernel on simplices 0 and 1.
Claim. The map $K_{\partial\delta}:\{0,\ldots,14\}\to\mathbb{R}$ sending each edge class $d$ to the sum of the two seed-simplex assemblies of the single-simplex deficit kernel (minus the local angle kernel) at flat: $K_{\partial\delta}(d)=A_0(K_{-\theta'})(d)+A_1(K_{-\theta'})(d)$, i.e. the class-space gradient $\partial(2\pi-\theta_0-\theta_1)/\partial\ell^2_{\mathrm{class}}$ restricted to the two seed cells sharing the hinge.
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 inside its two seed-cell Freudenthal 4-simplices only (permutations beginning $(0,1,\ldots)$); both share the same local squared-edge vector. The full lattice orbit sum and the flat Hessian of the 4D Regge action remain open.
The local angle kernel at flat is supported on two of the ten local edge slots (values $-1/4$ and $1/2$), obtained from the arccos chain factor $-1/\sin=-\sqrt{2}$ applied to the cosine derivatives. The single-simplex deficit kernel is the per-simplex contribution to $\delta=2\pi-\sum\theta$, namely minus that angle kernel. Assembly pushes a Fin-10 local kernel onto the 15 global edge classes by summing over local edges whose localEdgeClass matches the target class.
The present definition adds the two seed-simplex assemblies, yielding the two-simplex partial deficit class kernel $\partial(2\pi-\theta_0-\theta_1)/\partial\ell^2_{\mathrm{class}}$ at flat.
proof idea
Pure definition, not a proof. For each class index $d:\mathrm{Fin},15$, evaluate assembleClassKernel on simplex $0$ with the single-simplex deficit kernel, add the same assembly on simplex $1$, and return the sum. No tactics; the downstream value theorems discharge the concrete support and coefficients by simplifying the two assemblies against the incidence table.
why it matters
This is deliverable A item 4 in the module: the assembled two-simplex partial deficit gradient on the 15-class stencil. Downstream theorems pin its support and values: classes $3$ and $7$ equal $-1/2$, class $11$ equals $+1/2$, and it vanishes off ${3,7,11}$; a symmetry theorem shows invariance under the hinge-fixing axis swap $2\leftrightarrow 3$. Those facts are the concrete stencil data for any later orbit sum or Hessian assembly on the seed hinge.
In the broader QG campaign this is a checked local kernel, not a closure of Einstein–Hilbert recovery: the module explicitly does not flip gap_action_recovery or prove $S_{\mathrm{RS}}$ converges to EH in 4D. It sits one layer above the cosine and angle kernels and feeds every class-level identity about the partial deficit at flat.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.