oppDeficitKernel
plain-language theorem explainer
Opposite-orbit deficit class kernel on the 10-class local edge support: value 1/4 at class 2, -1/2 at class 9, and 0 elsewhere. It is the sparse weight pattern for the two opposite-type 4-simplices in the six-member Freudenthal star of the seed triangle hinge. Star assembly, member evaluations, and the opposite cosine chain identity cite it. The body is a pure case split on Fin 10.
Claim. Define the opposite-orbit deficit kernel $K_{\mathrm{opp}}:\{0,\ldots,9\}\to\mathbb{R}$ by $K_{\mathrm{opp}}(2)=1/4$, $K_{\mathrm{opp}}(9)=-1/2$, and $K_{\mathrm{opp}}(e)=0$ for every other edge class $e$.
background
In 4D Regge calculus on the integer lattice, curvature lives on triangular hinges. The seed hinge ${0,e_0,e_0+e_1}$ sits in a full periodic Freudenthal star: six incident 4-simplices across four unit cubes. Edge data are organized by a 15-class stencil; each simplex contribution is assembled on a 10-class local edge support.
The star splits into orbits. Opposite-orbit members (star indices 4 and 5) share one sparse weight pattern on that support. This module is the next kernel-checked increment after the dihedral cosine calculus: it imports the Freudenthal incidence layer and flat kernel, and never redefines their API. Scope is the seed hinge only; other lattice hinge orbits remain open.
proof idea
Definition by cases on $\mathrm{Fin},10$: index 2 maps to $1/4$, index 9 to $-1/2$, and every remaining index to $0$. No lemmas or tactics are used.
why it matters
Routes into the star-local deficit kernel, which sends star members 4 and 5 through this pattern. Private evaluation lemmas expand the assembled opposite-member contributions on the 15-class stencil; a chain identity equates the two nonzero entries to the opposite cosine kernel scaled by the chain-seed factor; a support lemma records vanishing off classes 2 and 9.
This is deliverable A item 4 of the QG full-theory campaign (full-star deficit class kernel on the seed hinge), a kernel-checked step after the dihedral kernel. It does not complete flat Hessian assembly over all hinges, does not prove $S_{\mathrm{RS}}$ converges to Einstein–Hilbert in 4D, and does not flip gap-action recovery.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.