fullStarClassKernel
plain-language theorem explainer
Lookup table for the type-(1,3) full-star deficit class kernel on the 15 edge-difference classes of the 4D Freudenthal lattice. It assigns ±√3 on the seven odd classes (1,3,5,7,9,11,13) and zero elsewhere. Cited by Bloch-fold and local-incidence assembly for the (1,3) hinge orbit. Pure definition by cases; no proof obligations.
Claim. The full-star deficit class kernel for the type-$(1,3)$ triangle hinge is the function $K:\{0,\ldots,14\}\to\mathbb{R}$ with $K(1)=K(3)=K(7)=K(13)=-\sqrt{3}$, $K(5)=K(9)=K(11)=+\sqrt{3}$, and $K(d)=0$ for all other class indices $d$.
background
In 4D Regge calculus on the periodic Freudenthal lattice, each triangle hinge sits in a star of Kuhn simplices. The deficit angle at the hinge, differentiated against edge-length squared perturbations and projected onto the 15 translation-invariant difference classes, yields a class kernel: a fixed vector in $\mathbb{R}^{15}$.
This module treats the type-$(1,3)$ hinge whose absolute masks are ${0,1,15}$ (difference masks $(1,14)$, local flat squared lengths $(1,3,4)$). Exactly six simplices in the origin cube contain the hinge; each has flat cosine $1/2$, so the star angle sum is $2\pi$ and the configuration is flat. Coordinate derivatives of the deficit are evaluated at the flat Gram point $(N,P,Q)=(8,8,8)$.
Sibling kernels already exist for orbits $(1,1)$, $(1,2)$, and $(2,2)$, with values in ${\pm 1}$, ${\pm\sqrt{2}/2}$, and ${\pm 1}$ respectively. The present table is the $(1,3)$ counterpart. Transport of this kernel to the complementary type $(3,1)$ remains open.
proof idea
Definition by exhaustive pattern match on Fin 15. Seven odd indices receive $\pm\sqrt{3}$ as listed; the catch-all clause returns $0$. No lemmas, tactics, or computational certificates are invoked at the definition site; the numerical values are the committed output of the upstream derivative-and-assembly campaign documented in the module (flat cosine multiset, ten coordinate derivatives, star enumeration).
why it matters
Delivers item 5 of the module's deliverable A: the full-star deficit class kernel for type $(1,3)$. Downstream Bloch-fold and local-incidence layers consume such kernels as the deficit factor in factorized slot terms, phased class dots, transported deficits, and orbit-mean local kernels (parallel to the $(1,1)$ wiring already present in ReggeBlochFold4D and ReggeBlochLocalIncidence4D).
In the Recognition Science gravity stack this is one more kernel-checked increment toward assembling the flat Hessian over all hinge orbits on the 4D lattice. It does not by itself close $S_{\mathrm{RS}}\to$ Einstein–Hilbert convergence, gap-action recovery, or reverse-engineered EH weights. The open transport to type $(3,1)$ via mask complement is the immediate next gap flagged by the module.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.