starLocalDeficitKernel
plain-language theorem explainer
Defines the per-member local deficit gradient kernel on the six-simplex Freudenthal star of the seed hinge: members 0–1 reuse the single-simplex angle kernel, 2–3 the orthogonal orbit kernel, and 4–5 the opposite orbit kernel. Gravity analysts assembling the full-star deficit class vector cite it. Pure pattern-match dispatch over the six star slots.
Claim. The local deficit kernel on the six-member star is the map $K:\{0,\ldots,5\}\times\{0,\ldots,9\}\to\mathbb{R}$ with $K(0,\cdot)=K(1,\cdot)$ equal to the single-simplex deficit kernel $-\theta'$, $K(2,\cdot)=K(3,\cdot)$ equal to the orthogonal-orbit deficit kernel, and $K(4,\cdot)=K(5,\cdot)$ equal to the opposite-orbit deficit kernel.
background
The module builds the full periodic-lattice star deficit class kernel for Regge calculus in 4D, one increment past the two-simplex dihedral cosine calculus. Scope is the seed triangle hinge ${0,e_0,e_0+e_1}$ and its complete Freudenthal star: four containing unit cubes and exactly six incident 4-simplices.
Deficit here means $\delta=2\pi-\sum\theta$, so each simplex contributes $-\theta'$ to the gradient. The single-simplex kernel is that contribution on the seed simplex. The orthogonal and opposite kernels are sparse vectors on the ten edge slots, encoding the flat Gram data of the two non-seed orbits (flat cosines $1/\sqrt{2}$ and $0$ respectively).
A parallel four-member kernel exists in the half-star module; this six-member version is the full-star counterpart used for the complete angle-sum and class-assembly gates.
proof idea
Definition by exhaustive pattern match on the star-member index in $\mathrm{Fin},6$. Indices $0$ and $1$ return the imported single-simplex deficit kernel; $2$ and $3$ return the orthogonal deficit kernel; $4$ and $5$ return the opposite deficit kernel. No computation beyond dispatch.
why it matters
This is the atomic lookup table that assembleStarMember folds against the star slot-class map to produce each member's contribution on the 15 edge-class stencil. The private evaluation lemmas for members 2–5 reduce through it by simplifying the sum to the sparse supports of the orthogonal and opposite kernels.
It fills deliverable A.4 of the module: the full-star deficit class kernel on classes $(2,3,6,7,10,11,14)$. Downstream gates (flatness $\sum\theta=2\pi$, nonvacuity, swap symmetry, scaling decoys, homothety stationarity) all consume the assembled vectors built from this kernel.
It does not close the flat Hessian over all hinge orbits, nor prove $S_{\mathrm{RS}}$ converges to Einstein–Hilbert in 4D, nor flip the gap-action recovery flag. Those remain open campaign targets.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.