fullStarClassKernelAssembled
plain-language theorem explainer
Assembled full-star deficit class kernel for the type-(2,2) Regge hinge: a map from the 15 edge-stencil classes to reals, summing the four star-member contributions. Gravity analysts cite it when equating the closed-form kernel to member-wise assembly, and when forming Bloch orbit means. The body is a direct finite sum over the four incident cube-translate/Kuhn-simplex pairs.
Claim. The assembled full-star class kernel $K^{\mathrm{asm}}_{\mathrm{star}}:\{0,\ldots,14\}\to\mathbb{R}$ for the type-$(2,2)$ hinge is $$K^{\mathrm{asm}}_{\mathrm{star}}(d)=\sum_{m=0}^{3} A_m(d),$$ where $A_m(d)$ is the contribution of the $m$-th star member (incident cube-translate/Kuhn-simplex pair) to stencil class $d$.
background
This module treats the type-(2,2) triangle hinge ${0,e_0+e_1,e_0+e_1+e_2+e_3}$ (masks ${0,3,15}$, difference masks $(3,12)$) on the 4D periodic Freudenthal lattice, as the next kernel-checked increment after the type-(1,1) seed orbit. Exactly four (cube translate, Kuhn simplex) pairs contain the hinge; the flat cosine multiset is identically zero and the star angle sum is $2\pi$.
The 15-class edge stencil partitions lattice edge directions into orbit classes under the residual symmetry. Each star member $m$ contributes a local deficit kernel on its ten edge slots; assembleStarMember bins those contributions by stencil class. Parallel assemblies exist for the (1,1), (1,2), and (1,3) orbits (with four or six members according to star cardinality).
The definition never redefines the Freudenthal incidence API, the Gram-projection cosine calculus, or the stencil; it only sums the already-constructed member maps.
proof idea
Pure definition: pointwise sum of the four member assemblies. For each stencil class $d$, evaluate $\sum_{m:\mathrm{Fin},4} A_m(d)$, where $A_m$ itself is the indicator-sum of the local deficit kernel over the ten edge slots whose star-slot class equals $d$. No lemmas are applied; the equality theorems that identify this assembly with the closed-form kernel live downstream.
why it matters
Delivers item 4 of the module's deliverable A: the full-star deficit class kernel on all 15 stencil classes, in assembled (member-sum) form. Downstream, fullStarClassKernel_eq proves this assembly equals the closed-form kernel; the Bloch incidence layer uses the same pattern for orbit-mean identities (e.g. equating orbit means to normalized assembled kernels on the (1,1) orbit). Sibling modules for (1,1), (1,2), and (1,3) mirror the same assembly shape, so cross-orbit comparisons stay uniform.
In the QG full-theory campaign this is a kernel-checked increment toward flat Hessian assembly over all hinges. It does not yet flip gap_action_recovery or prove $S_{\mathrm{RS}}$ converges to Einstein–Hilbert in 4D; those remain open. Landmark contact is the discrete curvature side of the Recognition gravity stack (Regge deficit as the local curvature observable), not the T0–T8 forcing chain directly.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.