partialDeficitClassKernel_seven
plain-language theorem explainer
At the flat Freudenthal seed hinge, the two-simplex partial deficit gradient with respect to squared edge length on global edge class 7 equals −1/2. Gravity analysts cite this when assembling the class-supported kernel of ∂(2π−θ₀−θ₁)/∂ℓ². The proof unfolds the two-simplex assembly, keeps only the active local slot whose class is 7, and reduces to the single-simplex slot-9 value.
Claim. At the flat seed configuration, the two-simplex partial deficit class kernel satisfies $\partial(2\pi-\theta_0-\theta_1)/\partial\ell^2_{\mathrm{class}\,7}=-1/2$.
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 partial deficit class kernel is the flat value of $\partial(2\pi-\theta_0-\theta_1)/\partial\ell^2$ assembled on the 15 global edge classes. It is the sum of two single-simplex assemblies (simplices $0$ and $1$), each of which only sees the two active local squared-edge slots $8$ and $9$ after the arccos chain rule at flat. The map localEdgeClass sends each local slot in a simplex to one of the 15 classes via the incidence mask.
Upstream, the assembly evaluation theorem reduces each simplex contribution to at most those two slots, and the single-simplex deficit kernel on slot $9$ is already known to be $-1/2$.
proof idea
Unfold the two-simplex definition, then rewrite each summand by the assembly evaluation theorem. Four decide comparisons on localEdgeClass show that only simplex $0$, slot $9$ lands in class $7$; the other three guards are false and contribute $0$. The surviving term is the single-simplex slot-$9$ kernel, already equal to $-1/2$, and norm_num closes the arithmetic.
why it matters
Module deliverable A lists the two-simplex partial deficit gradient as supported on classes $(3,7,11)$ with values $(-1/2,-1/2,+1/2)$. This theorem is the middle coordinate of that triple. Downstream, partialDeficitClassKernel_values packages the three equalities into one conjunction, and the hinge-fixing symmetry theorem uses the class-$7$ value (together with the class-$3$ twin under the $2\leftrightarrow 3$ swap) to prove invariance of the kernel. The result is a concrete, transcendental-free entry in the flat Hessian scaffolding for 4D Regge; it does not yet close the full orbit sum or the Einstein–Hilbert recovery gap.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.