fullStarClassKernel_values
plain-language theorem explainer
The type-(1,3) full-star deficit class kernel takes values ±√3 on Freudenthal edge classes 1,3,5,7,9,11,13 (four minus, three plus). Anyone closing the (1,3) star-kernel status flags or assembling the 4D Regge flat Hessian cites this table. The proof is pure definitional equality: seven reflexivity steps against the pattern-match arms.
Claim. For the type-$(1,3)$ full-star deficit class kernel $K:\{0,\ldots,14\}\to\mathbb{R}$, one has $K(1)=K(3)=K(7)=K(13)=-\sqrt{3}$ and $K(5)=K(9)=K(11)=\sqrt{3}$.
background
In the Regge 4D QG campaign, triangle hinges on the periodic Freudenthal lattice are typed by absolute masks. The type-(1,3) hinge uses masks ${0,e_0,e_0+e_1+e_2+e_3}={0,1,15}$ (difference masks $(1,14)$, local flat squared lengths $(1,3,4)$). Exactly six Kuhn simplices in the origin unit cube contain the hinge; each has flat cosine $1/2$, so the star angle sum is exactly $2\pi$.
The full-star deficit class kernel assigns a real weight to each of the 15 edge classes of the 4D stencil. Parallel kernels already exist for types $(1,1)$ (values in ${\pm 1}$), $(1,2)$ (values in ${\pm\sqrt{2}/2}$), and $(2,2)$ (values in ${\pm 1}$). This module records the $(1,3)$ table after the Gram-projection cosine calculus and the ten coordinate derivatives at flat values $(N,P,Q)=(8,8,8)$. Transport of the same kernel to the complementary type $(3,1)$ remains open.
proof idea
Term-mode one-liner. The goal is a seven-fold conjunction of equalities; each conjunct is witnessed by rfl. Every right-hand side matches a pattern-match arm of the local definition of the kernel on Fin 15, so definitional reduction closes the proof with no lemmas and no arithmetic.
why it matters
This is deliverable A.5 of the type-(1,3) star-kernel module: the explicit kernel table on classes $(1,3,5,7,9,11,13)$ with values $(-\sqrt{3},-\sqrt{3},+\sqrt{3},-\sqrt{3},+\sqrt{3},+\sqrt{3},-\sqrt{3})$. Downstream, hinge4DStarKernel13Status_flags sets fullStarClassKernelClosed = true from this theorem, while leaving type31TransportOpen and flatHessianAssemblyOpen true. Sibling value theorems for the $(1,1)$, $(1,2)$, and $(2,2)$ kernels sit in the same campaign layer. Together they feed the still-incomplete flat Hessian assembly over all hinges and the open goals $S_{\mathrm{RS}}$ converges to Einstein-Hilbert in 4D and gap-action recovery. No reverse-engineering of continuum EH weights is claimed.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.