fullStarClassKernel_nonvacuous
plain-language theorem explainer
The full-star deficit class kernel on the 15-class edge stencil is nonzero at class index 11, where its value is +1. Gravity analysts in the Regge 4D hinge campaign cite this as the nonvacuity gate for the seed-triangle periodic star. The proof is a one-line numerical reduction of the piecewise definition.
Claim. Let $K:\{0,\ldots,14\}\to\mathbb{R}$ be the full-star deficit class kernel on the 15-class stencil, with support on classes $(2,3,6,7,10,11,14)$ and values $(-1,-1,+1,-1,+1,+1,-1)$. Then $K(11)\neq 0$.
background
This module is the next kernel-checked increment in the QG full-theory Regge campaign after the dihedral cosine kernel. It treats the seed triangle hinge ${0,e_0,e_0+e_1}$ and its full periodic Freudenthal star in the integer lattice: four containing unit cubes and six incident 4-simplices. The 15-class edge stencil (imported, not redefined) labels edge orbits under the lattice symmetry that fixes the hinge.
The full-star deficit class kernel assigns a real weight to each of the 15 classes. On the supported classes $(2,3,6,7,10,11,14)$ the values are $(-1,-1,+1,-1,+1,+1,-1)$; all other classes map to zero. Nonvacuity of this kernel is one of the five gates listed in the module deliverable (alongside star enumeration, flat cosine multiset, flatness, and the remaining symmetry/scaling gates).
Sibling modules carry analogous kernels for other orbit representatives (with algebraic entries involving $\sqrt{2}$ or $\sqrt{3}$). The present kernel is the integer-valued seed case.
proof idea
One-line wrapper: unfold the piecewise definition of the full-star class kernel and discharge $K(11)\neq 0$ by norm_num. Class 11 is defined to return $+1$, so the inequality is immediate arithmetic.
why it matters
Nonvacuity is an explicit gate in the module deliverable list: without it the deficit class kernel could be the zero functional and would contribute nothing to the star action. Downstream, sibling nonvacuity theorems for the $\sqrt{2}$ and $\sqrt{3}$ orbit kernels mirror this gate, and the status-flag theorem in the type-(1,3) kernel module records fullStarClassKernelClosed = true as part of the campaign checklist.
The result sits inside the Regge 4D analysis layer that aims eventually at Einstein–Hilbert recovery of the RS action, but the module itself is careful: it does not assemble the flat Hessian over all hinges, does not prove $S_{\mathrm{RS}}$ converges to EH in 4d, and does not flip gap_action_recovery. It only certifies that this particular star kernel is a genuine nonzero class functional on the seed orbit.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.