fullStarClassKernelAssembled
plain-language theorem explainer
Assembled full-star deficit class kernel for the type-(1,3) Regge triangle hinge: a map from the 15 edge-orbit classes to reals obtained by summing the six Kuhn-simplex member contributions. Gravity analysts cite it when equating orbit-mean local kernels to explicit star sums. The body is the direct finite sum over star members.
Claim. Define the assembled full-star class kernel $K:\{0,\ldots,14\}\to\mathbb{R}$ by $K(d)=\sum_{m=0}^{5} A_m(d)$, where each $A_m$ bins the local type-$(1,3)$ deficit kernel of the $m$-th Kuhn simplex in the origin star onto the $15$ edge classes.
background
This module treats the Regge 4D type-(1,3) triangle hinge on the periodic lattice, with absolute masks ${0,1,15}$ (difference masks $(1,14)$, flat squared lengths $(1,3,4)$) and its full Freudenthal star. Exactly six Kuhn simplices in the origin unit cube contain the hinge; among cube translates in ${-1,0,1}^4$ only the origin does. All six share flat cosine $1/2$, so the star angle sum is exactly $2\pi$.
The sibling assembleStarMember bins one simplex: for member $m$ and class $d$ it sums the type-(1,3) local deficit kernel over the ten edge slots whose star-slot class equals $d$. The present definition stacks those six members. Parallel assembled kernels exist for types $(1,1)$, $(1,2)$, and $(2,2)$; the complementary type $(3,1)$ remains open for transport.
proof idea
Pure definition: pointwise sum of the six assembleStarMember maps over Fin 6. No lemmas, no tactics; the equality to the closed-form full-star kernel is proved separately by evaluating each member.
why it matters
Delivers item 5 of the module campaign: the full-star deficit class kernel on classes $(1,3,5,7,9,11,13)$ with target values $(-\sqrt{3},-\sqrt{3},+\sqrt{3},-\sqrt{3},+\sqrt{3},+\sqrt{3},-\sqrt{3})$. Downstream, fullStarClassKernel_eq identifies this assembled sum with the closed-form kernel; Bloch local-incidence theorems reuse the same assembly pattern for orbit means (type $(1,1)$ already equates orbit-mean local kernel to the assembled mean). It is the next kernel-checked increment after the type-$(1,1)$ seed orbit, still short of flat Hessian assembly over all hinges, $S_{\mathrm{RS}}\to\mathrm{EH}_{4d}$, and gap-action recovery.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.