fullStarClassKernel_eq
plain-language theorem explainer
For the type-(1,3) Regge triangle hinge, the six-member Freudenthal star sum equals the closed-form 15-class deficit kernel at every stencil index. Gravity analysts cite it when collapsing assembled star contributions to the tabulated kernel values (−√3, +√3 on the active classes). The proof expands the Fin-6 sum, rewrites each member to its closed form, then case-splits on Fin 15 and rings.
Claim. For every class index $d \in \{0,\ldots,14\}$, the assembled full-star contribution $\sum_{m=0}^{5} K_m(d)$ equals the closed-form type-$(1,3)$ full-star class kernel $K_{(1,3)}(d)$. Active classes are $(1,3,5,7,9,11,13)$ with values $(-\sqrt{3},-\sqrt{3},+\sqrt{3},-\sqrt{3},+\sqrt{3},+\sqrt{3},-\sqrt{3})$; all other classes vanish.
background
This module is the next kernel-checked increment in the QG full-theory campaign after the type-(1,1) seed orbit and the orbit classification layer. 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.
Exactly six Kuhn simplices contain the hinge; each has flat cosine $1/2$, so the star angle sum is $6\cdot(\pi/3)=2\pi$. The assembled kernel is the sum of six star-member contributions over the 15-class edge stencil. The closed-form kernel is the tabulated map on those fifteen classes. Upstream type-(1,1) and type-(1,2) modules prove the same assembly identity for their own member counts and algebraic values; this file mirrors that pattern for type $(1,3)$.
The complementary type $(3,1)$ is related by mask complement; transport of this kernel remains open.
proof idea
Unfold the assembled definition to a sum over Fin 6. Rewrite with the private six-term expansion lemma, then replace each of the six members by its closed-form evaluation lemma (member0_closed through member5_closed). Case-split on the fifteen stencil indices; on each branch simplify the closed-form kernel table and finish by ring normalization. No analytic estimates: pure finite algebraic identity.
why it matters
Closes deliverable A.5 of the type-(1,3) star kernel: the full-star deficit class kernel is kernel-checked and equals its assembled sum. Downstream, the status-flags theorem records fullStarClassKernelClosed = true. Sibling modules for types (1,1), (1,2), and (2,2) use the same assembly-equality pattern; Bloch local-incidence theorems for the (1,1) orbit already consume the analogous identity to equate orbit-mean local kernels with assembled means.
In the broader campaign this is one hinge-type brick toward flat Hessian assembly and eventual comparison with Einstein–Hilbert. It does not flip gap_action_recovery, does not prove S_RS_converges_EH_4d, and leaves type-(3,1) transport open. No direct appeal to T0–T8 or the Recognition Composition Law; the link is through the discrete gravity / Regge side of the monolith.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.