fullStarClassKernel_values
plain-language theorem explainer
Records the fifteen explicit real values of the full-star deficit class kernel for the type-(2,2) Regge triangle hinge on the 4D periodic Freudenthal lattice. Gravity analysts cite it when assembling the flat Hessian or checking kernel closure gates. The proof is a pure term of fifteen reflexivity steps against the piecewise definition.
Claim. For the type-$(2,2)$ hinge orbit, the full-star deficit class kernel $K:\{0,\ldots,14\}\to\mathbb{R}$ evaluates as $K(0)=1$, $K(1)=1$, $K(2)=-1$, $K(3)=1$, $K(4)=-1$, $K(5)=-1$, $K(6)=1$, $K(7)=1$, $K(8)=-1$, $K(9)=-1$, $K(10)=1$, $K(11)=-1$, $K(12)=1$, $K(13)=1$, $K(14)=-1$.
background
This module treats the Regge 4D full periodic-lattice star for the type-(2,2) triangle hinge with vertex masks ${0,3,15}$ (difference masks $(3,12)$). The campaign imports the Freudenthal incidence layer, the 15-class edge stencil, and the Gram-projection cosine calculus without redefining their APIs.
The full-star class kernel assigns a real weight to each of the fifteen stencil classes that appear when edge lengths are varied about the flat embedding. Sibling modules record the analogous kernels for the $(1,1)$, $(1,2)$ and $(1,3)$ orbits; those kernels involve $\pm 1$, $\pm\sqrt{2}/2$ or $\pm\sqrt{3}$ on sparse supports. For type $(2,2)$ the support is full and every entry is $\pm 1$.
Upstream, star enumeration already shows exactly four (cube translate, Kuhn simplex) pairs contain the hinge, each with flat cosine $0$, so the star angle sum is exactly $2\pi$. The kernel values sit on top of that flatness gate.
proof idea
The definition of the kernel is a total function on Fin 15 given by fifteen literal real constants. The theorem is the conjunction of the fifteen equalities obtained by evaluating that definition at each index. The term proof is simply the 15-tuple of rfl constructors; no lemmas or rewriting are required.
why it matters
Deliverable A.4 of the type-(2,2) star-kernel increment in the QG full-theory campaign. Closing the kernel lets the module raise the fullStarClassKernelClosed status flag (parallel to the flags already proved for the $(1,1)$, $(1,2)$ and $(1,3)$ orbits). Downstream status theorems and cross-orbit kernel-value statements consume this conjunction when they assert that every hinge orbit now has an explicit, kernel-checked weight vector.
The result does not yet assemble the flat Hessian over all hinges, nor does it prove $S_{\mathrm{RS}}$ converges to Einstein–Hilbert in 4D, nor does it flip gap_action_recovery. It is the concrete numerical input those later steps will need once every orbit is closed. Within the Recognition forcing chain it sits inside the gravity analysis layer that ultimately supports the continuum limit after T8 ($D=3$ spatial, here lifted to 4D spacetime Regge).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.