fullStarClassKernel
plain-language theorem explainer
The type-(1,2) full-star deficit class kernel maps each of the 15 edge-stencil classes to ±√2/2 on the periodic Freudenthal star of the triangle hinge {0, e₀, e₀+e₁+e₂}. Gravity analysts cite it when building orbit-mean local kernels and factorized Bloch folds for that hinge orbit. The body is an exhaustive case table on Fin 15; no proof obligations.
Claim. The full-star deficit class kernel for the type-$(1,2)$ Regge hinge is the function $K:\{0,\ldots,14\}\to\mathbb{R}$ with $K(i)=\pm\sqrt{2}/2$, negative on classes $0,5,6,9,10,11,12$ and positive on $1,2,3,4,7,8,13,14$.
background
In 4D Regge calculus on the integer lattice, a triangle hinge sits in a Freudenthal star of incident 4-simplices. The module treats the type-(1,2) representative hinge ${0,e_0,e_0+e_1+e_2}$ (masks $0,1,7$; difference masks $(1,6)$): two containing unit cubes and four incident simplices. The 15-class edge stencil partitions lattice edge directions into translation orbits used for deficit bookkeeping.
Sibling modules supply the same interface for other orbits: type $(1,1)$ uses integer values $\pm 1$, type $(1,3)$ uses $\pm\sqrt{3}$, and type $(2,2)$ uses $\pm 1$. This module is the next kernel-checked increment after the $(1,1)$ seed orbit. Flat cosines on the four simplices are all $0$, so the star angle sum is exactly $2\pi$ and the deficit vanishes in the flat background; the kernel records the first-order class weights under edge-length perturbation.
The committed Gram-projection / cleared-denominator cosine calculus and the Freudenthal incidence layer are imported, not redefined.
proof idea
Pure definition by exhaustive pattern match on Fin 15. Each constructor index is assigned either $\sqrt{2}/2$ or $-\sqrt{2}/2$; there is no tactic proof, no lemma application, and no computational certificate inside the declaration itself. Downstream theorems treat the table as the committed numerical kernel for the $(1,2)$ orbit.
why it matters
Deliverable A.4 of the type-(1,2) star module: the full-star deficit class kernel with values $\pm\sqrt{2}/2$ on all 15 stencil classes. It is the numerical seed that orbit-mean local kernels, transported deficits, and factorized Bloch-fold slot terms consume when assembling the quadratic form on this hinge orbit (parallel to how the $(1,1)$ kernel feeds factorizedSlotTerm, transportedDeficit, and orbitMeanLocalKernel_t11 in the Bloch-fold and local-incidence layers).
In the Recognition Science gravity campaign this is one orbit toward the flat Hessian of the Regge action on the periodic lattice, a prerequisite for comparing the discrete action to Einstein–Hilbert continuum recovery. It does not by itself flip gap_action_recovery or prove S_RS_converges_EH_4d. The complement type $(2,1)$ and all other hinge orbits remain open in this module.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.