fullStarClassKernelAssembled
plain-language theorem explainer
Assembled full-star deficit class kernel for the type-(1,2) triangle hinge: a map from the fifteen edge-length stencil classes to reals, obtained by summing four star-member contributions. Cited by anyone equating the closed-form kernel to the star sum, or building Bloch orbit means for this hinge orbit. Pure definition: one-line sum over the four incident 4-simplices.
Claim. The assembled full-star class kernel $K:\{0,\ldots,14\}\to\mathbb{R}$ is defined by $K(d)=\sum_{m=0}^{3} A_m(d)$, where each $A_m$ is the contribution of the $m$-th incident 4-simplex in the Freudenthal star of the type-$(1,2)$ hinge $\{0,e_0,e_0+e_1+e_2\}$, routing that simplex's local deficit-kernel entries onto the fifteen stencil classes.
background
This module treats the Regge 4D full periodic-lattice star for hinge type $(1,2)$: the triangle ${0,e_0,e_0+e_1+e_2}$ (masks $0,1,7$; difference masks $(1,6)$). The full Freudenthal star consists of exactly four incident 4-simplices in two containing unit cubes of the integer lattice. The campaign imports the Freudenthal incidence layer, the fifteen-class edge stencil, and the committed Gram-projection cosine calculus without redefining their API.
Each star member $m\in{0,1,2,3}$ contributes a map $A_m$ that, for every stencil class $d$, sums the local deficit-kernel values on those of the ten edges whose slot class equals $d$. The assembled kernel is the sum of these four maps. Flat cosines on all four simplices are $0$, so the star angle sum is exactly $2\pi$ (flatness gate). The closed-form kernel on the fifteen classes takes values in ${\pm\sqrt{2}/2}$.
The type-$(1,1)$ seed orbit (six members) and the related $(1,3)$ and $(2,2)$ modules use the same assemble-then-sum pattern with different cardinalities and local kernels.
proof idea
Definition only: pointwise sum $K(d)=\sum_{m:\mathrm{Fin},4} A_m(d)$, where $A_m$ is the in-module star-member assembler (sum over ten edges, keep the local deficit kernel when the slot class matches $d$, else zero). No lemmas, no tactics.
why it matters
Delivers item 4 of the module's deliverable A: the full-star deficit class kernel on all fifteen stencil classes for type $(1,2)$. The equality theorem in this module identifies the assembled sum with the closed-form kernel (values $\pm\sqrt{2}/2$), after expanding the four-member sum and simplifying square-root coefficients.
Downstream, the Bloch local-incidence layer uses the same assemble/full-star pattern (for the $(1,1)$ orbit) to equate orbit-mean local kernels to normalized assembled means and to prove star-assembly identities. Parallel assembled kernels in the $(1,1)$, $(1,3)$, and $(2,2)$ modules share the interface so orbit means can be compared across hinge types.
This is one kernel-checked increment in the QG full-theory campaign toward a flat Hessian over all hinges. It does not finish that assembly, does not prove RS action convergence to Einstein–Hilbert in 4D, and does not flip gap-action recovery. Complement type $(2,1)$ and other hinge orbits remain open.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.