fullStarClassKernelAssembled
plain-language theorem explainer
Defines the assembled full-star deficit class kernel on the 15 edge-orbit classes by summing the six star-member contributions at each class. Anyone checking the seed-hinge Regge star flat Hessian or Bloch orbit means cites it. The body is a one-line finite sum over the six Freudenthal star members.
Claim. For each edge class $d \in \{0,\ldots,14\}$, the assembled full-star class kernel equals $\sum_{m=0}^{5} K_m(d)$, where $K_m$ is the class-kernel contribution of the $m$-th star member (cube translate paired with Kuhn 4-simplex) of the seed triangle hinge.
background
The module builds the full periodic-lattice star deficit class kernel for the seed hinge ${0,e_0,e_0+e_1}$ in the 4D Freudenthal–Kuhn triangulation. Exactly six (cube translate, Kuhn simplex) pairs contain that hinge; other hinge orbits remain open.
Each star member $m$ contributes a local map $K_m:\mathrm{Fin},15\to\mathbb{R}$ that, for class $d$, sums the member's local deficit kernel over the ten edge slots whose stencil class equals $d$. The fifteen classes are the edge-orbit labels of the 4D Regge edge stencil.
The surrounding campaign imports the dihedral cosine calculus and flat kernel; it never redefines those APIs. Deliverable A targets the full-star kernel on classes $(2,3,6,7,10,11,14)$ with values $(-1,-1,+1,-1,+1,+1,-1)$, plus flatness and stationarity gates.
proof idea
Pure definition: pointwise sum of the six already-defined member assemblers. No tactics, no lemmas inside the body. Downstream equality theorems expand the sum via a six-term rewrite and evaluate each member.
why it matters
This is the assembly side of the full-star deficit class kernel for the seed hinge, the QG full-theory increment after the dihedral kernel. It is the object equated to the closed-form fullStarClassKernel and the witness that the member sum equals the full star.
Bloch local-incidence theorems use it to identify the $t_{11}$ orbit-mean local kernel with six-inverse times this assembled map, and to rewrite the six-member sum as the full-star kernel. Parallel assemblers exist for the $t_{12}$, $t_{13}$, and $t_{22}$ orbits.
It does not finish flat Hessian assembly over all hinges, does not prove $S_{\mathrm{RS}}$ converges to Einstein–Hilbert in 4D, and does not flip gap-action recovery. It sits inside the gravity analysis layer that feeds continuum recovery, not the T0–T8 forcing chain itself.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.