fullStarClassKernel_values
plain-language theorem explainer
For the type-(1,2) Regge triangle hinge, the full-star deficit class kernel on the 15-class edge stencil evaluates to −√2/2 at classes 0 and 5, and +√2/2 at classes 1 and 14. Anyone checking the flat Hessian assembly or the kernel gates for this orbit cites this. The proof is pure definitional equality: four reflexivity steps against the piecewise definition.
Claim. Let $K:\{0,\ldots,14\}\to\mathbb{R}$ be the full-star deficit class kernel for the type-$(1,2)$ hinge orbit. Then $K(0)=-\sqrt{2}/2$, $K(1)=\sqrt{2}/2$, $K(5)=-\sqrt{2}/2$, and $K(14)=\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 in the integer lattice: two containing unit cubes and four incident 4-simplices. It sits in the QG full-theory campaign as the next kernel-checked increment after the type-(1,1) seed orbit.
The 15-class edge stencil classifies squared-length orbits around the hinge. The full-star deficit class kernel $K$ assigns to each class the contribution that enters the linearized deficit (angle-sum) variation once the star is assembled. Upstream modules fix the same API for other orbits: type (1,1) uses integer values $\pm 1$ on a different support; type (1,3) uses $\pm\sqrt{3}$; type (2,2) again uses $\pm 1$.
Local deliverables already closed before this theorem include star enumeration (exactly four cube-translate/Kuhn-simplex pairs), flat cosine multiset (all four simplices have flat cosine $0$), and the flatness gate (star angle sum equals $2\pi$).
proof idea
Term-mode proof by four reflexivity steps. The local piecewise definition of the kernel already sends Fin indices $0$ and $5$ to $-\sqrt{2}/2$ and indices $1$ and $14$ to $+\sqrt{2}/2$, so each conjunct is definitionally true. No lemmas are applied.
why it matters
Closes deliverable A.4 of the type-(1,2) star-kernel module: the full-star deficit class kernel on all 15 stencil classes takes values in ${\pm\sqrt{2}/2}$ on the stated support. Downstream, sibling orbit modules (type (1,1), (1,3), (2,2)) mirror the same values theorem pattern, and the type-(1,3) status-flags theorem records fullStarClassKernelClosed = true once its own values theorem is in place; this declaration is the (1,2) counterpart of that gate.
In the broader Recognition gravity stack the kernel feeds the flat Hessian of the Regge action on the periodic lattice. It does not yet assemble that Hessian over all hinge orbits, nor does it touch $S_{\mathrm{RS}}\to$ Einstein–Hilbert convergence or gap-action recovery. The complement-related type-(2,1) orbit remains open and is not transported here. Framework landmark: this is discrete 4D geometry on the eight-tick / $D=3$ lattice side of the forcing chain, not a continuum curvature identity.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.