fullStarClassKernel_nonvacuous
plain-language theorem explainer
The type-(1,3) full-star deficit class kernel is nonzero at class 5, where its value is √3. Gravity analysts in the QG full-theory campaign cite this as the nonvacuity gate for the (1,3) star kernel. The proof unfolds the kernel definition at that slot and applies the standard real square-root nonvanishing lemma.
Claim. Let $K:\{0,\ldots,14\}\to\mathbb{R}$ be the full-star deficit class kernel of the type-$(1,3)$ Regge hinge (values $\pm\sqrt{3}$ on the odd classes $1,3,5,7,9,11,13$ and zero elsewhere). Then $K(5)\neq 0$.
background
This module treats the Regge 4D type-(1,3) periodic-lattice star on the triangle hinge with absolute masks ${0,1,15}$ (difference masks $(1,14)$, local flat squared lengths $(1,3,4)$). Exactly six Kuhn simplices in the origin unit cube contain the hinge; each has flat cosine $1/2$, so the star angle sum is $2\pi$ and the configuration is flat.
The full-star deficit class kernel aggregates ten coordinate derivatives of the deficit (via the cleared-denominator master lemma at flat values $(N,P,Q)=(8,8,8)$) into the 15-class stencil. On classes $(1,3,5,7,9,11,13)$ the assembled kernel takes values $(-\sqrt{3},-\sqrt{3},+\sqrt{3},-\sqrt{3},+\sqrt{3},+\sqrt{3},-\sqrt{3})$; elsewhere it is zero. Parallel nonvacuity gates already exist for the type-$(1,1)$ and type-$(1,2)$ kernels (values $\pm 1$ and $\pm\sqrt{2}/2$ respectively).
proof idea
Term-mode one-liner. Unfolding the kernel definition at index 5 rewrites the goal to $\sqrt{3}\neq 0$. Discharge by Real.sqrt_ne_zero' after a norm_num proof that $0<3$. No star-assembly lemmas are needed; the closed-form case table already pins the value.
why it matters
Nonvacuity is deliverable A item 6 in the module brief: one of the four gates (nonvacuity, hinge-fixing axis swap $1\leftrightarrow 2$, uniform-scaling decoy, homothety stationarity) that close the type-(1,3) full-star class kernel. Downstream, hinge4DStarKernel13Status_flags records fullStarClassKernelClosed = true from this fact (together with the enumeration and flatness gates).
Sibling nonvacuity theorems for the $(1,1)$ and $(1,2)$ orbits, and the parallel claim in the $(2,2)$ module, form the same gate pattern across hinge types. The result does not transport the kernel to the complementary type $(3,1)$ (explicitly OPEN) and does not complete flat Hessian assembly or flip gap_action_recovery / S_RS_converges_EH_4d.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.