fullStarClassKernel_nonvacuous
plain-language theorem explainer
Nonvacuity gate for the type-(2,2) full-star deficit class kernel on the 15-class Regge edge stencil: the kernel at class index 0 is a nonzero real. Gravity analysts assembling flat Hessians over Freudenthal stars cite it as the first kernel gate after star enumeration and flatness. Proof is a one-line norm_num unfold of the closed-form kernel definition.
Claim. For the type-$(2,2)$ Regge triangle hinge on the 4D periodic lattice, the full-star deficit class kernel $K:\mathrm{Fin}\,15\to\mathbb{R}$ satisfies $K(0)\neq 0$.
background
This module treats the type-(2,2) triangle hinge ${0,e_0+e_1,e_0+e_1+e_2+e_3}$ (masks ${0,3,15}$, difference masks $(3,12)$) and its full periodic Freudenthal star in 4D Regge calculus. The campaign imports the Freudenthal incidence layer, the 15-class edge stencil, and the Gram-projection cosine calculus without redefining their API.
The full-star class kernel is a closed-form map from the 15 stencil classes to $\mathbb{R}$, recording the aggregated deficit contribution of the star after flat cosine evaluation. Sibling modules close the same gate for other hinge orbits: type $(1,1)$ seed, type $(1,2)$, and type $(1,3)$, each with its own sparse support on $\mathrm{Fin},15$.
Local deliverables already include star enumeration (exactly four cube-translate/Kuhn-simplex pairs), flat cosine multiset (all four incident simplices have cosine $0$), and the flatness gate (star angle sum equals $2\pi$). Nonvacuity is the first of the remaining gates listed in the module brief.
proof idea
One-line wrapper. Unfold the local closed-form definition of the full-star class kernel at index $0$, then discharge the resulting numeric inequality by norm_num. No lemmas beyond the definition itself are required; the same pattern appears in the type-$(1,1)$ nonvacuity theorem (there at index 11) and the type-$(1,2)$ gate (index 0, with an explicit $\sqrt{2}\neq 0$ step).
why it matters
Closes the nonvacuity gate for the type-(2,2) orbit inside the QG full-theory campaign, the next kernel-checked increment after the type-$(1,1)$ seed star. Downstream, sibling nonvacuity theorems for the $(1,1)$, $(1,2)$, and $(1,3)$ orbits mirror this gate, and the type-$(1,3)$ status-flag theorem packages the corresponding fullStarClassKernelClosed = true bit alongside star-enumeration and flatness flags.
Within Recognition Science gravity analysis this is bookkeeping infrastructure for assembling the flat Hessian over all hinge orbits on the periodic lattice. It does not yet touch the continuum limit $S_{\mathrm{RS}}\to S_{\mathrm{EH}}$ in 4D, nor the gap-action recovery flag. The module brief is explicit that other hinge orbits remain previously closed or still open, and that reverse-engineering weights from Einstein–Hilbert is out of scope.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.