t13DeficitKernel
plain-language theorem explainer
Explicit ten-slot deficit kernel for the type-(1,3) Regge triangle hinge on the 4D periodic lattice: nonzero only at edge indices 4, 6, 7, 9 with values −√3/6, √3/4, √3/4, −√3/2. Gravity analysts cite it when assembling full-star class vectors for the (1,3) Freudenthal star. Pure pattern-match definition; no proof obligations.
Claim. Define the type-$(1,3)$ star deficit kernel $K_{13}:\{0,\ldots,9\}\to\mathbb{R}$ by $K_{13}(4)=-\sqrt{3}/6$, $K_{13}(6)=\sqrt{3}/4$, $K_{13}(7)=\sqrt{3}/4$, $K_{13}(9)=-\sqrt{3}/2$, and $K_{13}(e)=0$ for every other edge index $e$.
background
This module is the next kernel-checked increment in the 4D Regge QG campaign after the type-(1,1) seed orbit. It treats the type-(1,3) triangle hinge with absolute masks ${0,1,15}$ (difference masks $(1,14)$, local flat squared lengths $(1,3,4)$) and its full periodic Freudenthal star inside the origin unit cube and its ${-1,0,1}^4$ translates.
The ten coordinates are the edge slots of the local stencil. The deficit class kernel records the contribution of each slot to the star angle-deficit after the flat cosine multiset (all six Kuhn simplices share flat cosine $1/2$) and the cleared-denominator derivative calculus at flat values $(N,P,Q)=(8,8,8)$ have been applied. Complementary type $(3,1)$ is related by mask complement; transport of this kernel remains open.
Downstream assembly folds the kernel against a star-slot-to-class map, producing a vector on the 15-class stencil used for nonvacuity, hinge-fixing, and stationarity gates.
proof idea
Definition by exhaustive pattern match on Fin 10. Four constructors return the explicit algebraic constants involving $\sqrt{3}$; the catch-all clause returns $0$. No lemmas, tactics, or computational search are involved.
why it matters
This is deliverable A.5 of the module: the full-star deficit class kernel that feeds every subsequent assembly step. assembleStarMember sums the kernel over the ten edge slots against the star-slot class map, producing one 15-class vector per star member. The private closed-form lemmas member0_closed through member5_closed then expand those sums into sparse if-then expressions on classes ${1,3,5,7,9,11,13}$, and deficit_zero_off records that the kernel vanishes off ${4,6,7,9}$.
Those closed forms underwrite the module gates (nonvacuity, hinge-fixing transposition $1\leftrightarrow 2$ of axes ${1,2,3}$, uniform-scaling decoy, homothety stationarity exactly $0$). In the broader Recognition gravity stack this is a concrete kernel check on the Regge side of the Einstein–Hilbert recovery path; it does not yet flip gap_action_recovery or prove $S_{\mathrm{RS}}$ converges to EH in 4D, and it does not reverse-engineer weights from the continuum action.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.