fullStarClassKernel_nonvacuous
plain-language theorem explainer
The type-(1,2) full-star deficit class kernel is nonzero at stencil class 0, where its value is −√2/2. Gravity analysts cite this as the nonvacuity gate for the (1,2) Regge hinge orbit on the periodic Freudenthal lattice. The proof is a two-line reduction: √2 ≠ 0, then unfold the piecewise definition.
Claim. Let $K:\{0,\ldots,14\}\to\mathbb{R}$ be the full-star deficit class kernel for the type-$(1,2)$ triangle hinge on the 4D periodic Freudenthal lattice. Then $K(0)\neq 0$. Explicitly, $K(0)=-\sqrt{2}/2$.
background
This module treats the type-(1,2) triangle hinge ${0,e_0,e_0+e_1+e_2}$ (masks $0,1,7$; difference masks $(1,6)$) and its full periodic Freudenthal star: two containing unit cubes and four incident 4-simplices. The campaign sits in the QG full-theory stack after the type-(1,1) seed orbit, reusing the Freudenthal incidence layer, the 15-class edge stencil, and the committed Gram-projection cosine calculus.
The full-star class kernel $K:\mathrm{Fin},15\to\mathbb{R}$ records the net signed contribution of each stencil class to the star deficit. For type (1,2) the nonzero entries are $\pm\sqrt{2}/2$ on the first five classes (class 0 carries $-\sqrt{2}/2$). Parallel kernels exist for the (1,1), (1,3), and (2,2) orbits, with different algebraic values ($\pm 1$, $\pm\sqrt{3}$, etc.).
Nonvacuity is one of the five gates listed in the module deliverable: the kernel must not be the zero function, otherwise the star contributes nothing to the discrete curvature assembly.
proof idea
Term-style tactic proof. First obtain $\sqrt{2}\neq 0$ from Real.sqrt_ne_zero' and norm_num on $0<2$. Then simp unfolds fullStarClassKernel at index $0$, which is defined as $-\sqrt{2}/2$, and discharges the inequality with the square-root fact. No induction or case split beyond the piecewise definition.
why it matters
Closes the nonvacuity gate for deliverable A of the type-(1,2) star-kernel module (item 5: gates include nonvacuity, swap symmetry, uniform-scaling decoy, and homothety stationarity). Downstream status aggregators and the sibling nonvacuity theorems for orbits (1,1), (1,3), and (2,2) pattern-match on the same gate shape; one consumer is hinge4DStarKernel13Status_flags, which packages enumeration, flatness, and kernel-closed bits.
In the broader Recognition gravity stack this is a kernel-checked increment toward discrete Einstein–Hilbert recovery on the 4D lattice, consistent with the forced spatial dimension $D=3$ (forcing step T8) once the full hinge orbit set is closed. It does not yet assemble the flat Hessian over all hinges, nor prove $S_{\mathrm{RS}}$ converges to EH in 4D, nor discharge gap_action_recovery. The complement orbit (2,1) remains explicitly open.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.