fullStarClassKernel_values
plain-language theorem explainer
The full-star deficit class kernel on the 15-class Regge edge stencil takes the signed values (-1,-1,+1,-1,+1,+1,-1) at classes 2, 3, 6, 7, 10, 11, and 14. Gravity analysts assembling the 4D Freudenthal-star linearized deficit or closing flatness gates cite this table. The proof is pure definitional unfolding: seven reflexivity steps on the case-split definition.
Claim. The full-star class kernel $K:\{0,\ldots,14\}\to\mathbb{R}$ satisfies $K(2)=-1$, $K(3)=-1$, $K(6)=1$, $K(7)=-1$, $K(10)=1$, $K(11)=1$, and $K(14)=-1$.
background
In the Regge 4D full-theory campaign the seed triangle hinge ${0,e_0,e_0+e_1}$ sits in a full periodic Freudenthal star: four containing unit cubes and six incident 4-simplices on the integer lattice. Edge variations are organized by a fixed 15-class stencil. The full-star deficit class kernel assigns a real weight to each class; those weights enter the linearized angle-sum (deficit) response of the star under edge stretch.
This module imports the dihedral-cosine kernel, the flat Gram kernel, and the edge stencil, and never redefines their APIs. Sister orbit modules supply analogous kernels with $\sqrt{2}$ or $\sqrt{3}$ entries; the present kernel is the integer-valued pattern on the complementary classes $(2,3,6,7,10,11,14)$. Module scope is deliberately the seed hinge orbit only; other lattice hinge orbits remain open.
proof idea
The kernel is a Fin 15 → ℝ definition by pattern match, returning the constants $-1$ or $+1$ on the seven listed indices. Each conjunct of the theorem is therefore a definitional equality. The proof term is the seven-fold product of rfl, one per conjunct; no lemmas or arithmetic are required.
why it matters
This is deliverable A.4 of the module: the explicit full-star deficit class kernel table with values $(-1,-1,+1,-1,+1,+1,-1)$. Parallel value theorems in the 12-, 13-, and 22-orbit modules mirror the same pattern for their own kernels. Downstream status flags (for example the 13-orbit status theorem) set fullStarClassKernelClosed = true once these tables are in place, while leaving type-3-1 transport and flat Hessian assembly open.
The table feeds nonvacuity, swap-$2\leftrightarrow 3$ symmetry, uniform-scaling decoy, and homothety-stationarity gates. It is a kernel-checked increment toward discrete-to-continuum gravity in the Recognition stack, still short of proving RS action convergence to Einstein–Hilbert in 4D or closing gap-action recovery. Spatial dimension $D=3$ (forcing step T8) is the ambient setting; the present result does not yet assemble the full Hessian over all hinges.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.