assembleStarMember
plain-language theorem explainer
For each of the six Kuhn simplices around a type-(1,3) triangle hinge, this builds the contribution of that simplex to the global 15-class deficit kernel. It scatters the ten local edge weights of the type-(1,3) deficit kernel onto the 15 edge classes via the slot-class map. Exact-action and Bloch-incidence layers cite it when contracting phased star deficits. The body is a pure definitional scatter-sum.
Claim. For each star member $m\in\{0,\ldots,5\}$, define a map on the $15$ edge classes by $d\mapsto\sum_{e=0}^{9}\mathbf{1}_{\mathrm{slot}(m,e)=d}\,K_{13}(e)$, where $K_{13}$ is the type-$(1,3)$ local deficit kernel on the ten coordinate edges and $\mathrm{slot}(m,\cdot)$ is the local-slot-to-class assignment after reordering the hinge to $(0,1,15)$.
background
This module treats the type-(1,3) triangle hinge on the 4D periodic Freudenthal lattice, with absolute masks ${0,1,15}$ (difference masks $(1,14)$, flat squared lengths $(1,3,4)$). Exactly six Kuhn simplices in the origin unit cube contain the hinge; their flat dihedral cosines are all $1/2$, so the star angle sum is exactly $2\pi$.
The ambient calculus uses a fixed $15$-class edge stencil on the lattice and a local ten-edge labeling per simplex. The local-to-global map starSlotClass sends each of the six members' ten slots to a class in $\mathrm{Fin},15$ after hinge reordering along the Freudenthal chain. The weights themselves come from t13DeficitKernel: nonzero only on four slots, with values $-\sqrt{3}/6$, $\sqrt{3}/4$, $\sqrt{3}/4$, $-\sqrt{3}/2$.
Parallel assemblers exist for type $(1,1)$ (six members) and type $(1,2)$ (four members); this definition is the $(1,3)$ instance of the same scatter pattern.
proof idea
Definitional one-liner. For fixed star member $m$, the value at class $d$ is the sum over the ten local edges $e$ of the indicator that starSlotClass m e equals $d$, times the scalar t13DeficitKernel e. No lemmas are applied; the body is the scatter-sum itself.
why it matters
This is deliverable A.5 of the type-(1,3) star kernel: the per-member class kernel that, once summed over the six members, yields the full-star deficit on classes $(1,3,5,7,9,11,13)$ with values $(-\sqrt{3},-\sqrt{3},+\sqrt{3},-\sqrt{3},+\sqrt{3},+\sqrt{3},-\sqrt{3})$. Downstream, Regge4DExactActionSymbol pushes these assemblers by covering permutations and contracts them against wave covectors (phased deficit dots for the various hinge types). ReggeBlochLocalIncidence4D uses the same pattern for star-assembly identities such as member-sum equals full star.
In the QG campaign it is the next kernel-checked increment after the type-$(1,1)$ seed orbit. 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. Transport of this kernel to the complementary type $(3,1)$ remains open.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.