assembleStarMember
plain-language theorem explainer
For each of the four star members of the type-(1,2) Regge hinge, builds the 15-class deficit vector by routing that member's ten local edge deficits into stencil slots. Anyone assembling the full-star kernel, phased deficit contractions, or Bloch incidence sums for orbit (1,2) cites this. Pure definitional sum: conditional accumulation of the local deficit kernel under the slot-class map.
Claim. For each star-member index $m\in\{0,1,2,3\}$, the assembled class vector is the map $d\mapsto\sum_{e=0}^{9} K_m(e)\,\mathbf{1}_{c(m,e)=d}$, where $K_m$ is the local deficit kernel on the ten edges of member $m$ and $c(m,e)\in\{0,\ldots,14\}$ is the stencil slot class of edge $e$ in that member.
background
Module setting: the type-(1,2) triangle hinge ${0,e_0,e_0+e_1+e_2}$ (masks $0,1,7$) and its full periodic Freudenthal star in the integer lattice: two containing unit cubes, four incident 4-simplices. This is the next kernel-checked increment after the type-(1,1) seed orbit. The 15-class edge stencil and the committed Gram-projection cosine calculus are imported, not redefined.
Each star member $m$ carries a local deficit kernel on ten edges (near-orbit for $m\in{0,1}$, far-orbit for $m\in{2,3}$), with values in ${\pm\sqrt{2}/2}$ after flat cosine evaluation. The slot-class map sends each (member, edge) pair to one of the fifteen global stencil classes, encoding how that edge sits relative to the hinge under the cube translate and Kuhn simplex of the member.
The type-(1,1) sibling uses the same assembly pattern over six members; here the star cardinality is four, matching the enumeration proved in this module.
proof idea
Definitional one-liner. For fixed member $m$, the output at class $d$ is the sum over the ten local edges $e$ of the local deficit kernel value when the slot class equals $d$, and zero otherwise. No lemmas are applied; the body is the conditional sum itself, parallel to the type-(1,1) and type-(1,3) assemble definitions.
why it matters
This is the per-member building block of the full-star deficit class kernel for orbit (1,2), deliverable A.4 of the module (values $\pm\sqrt{2}/2$ on the 15 stencil classes). Downstream, phasedDeficitDotResolvedT12 contracts the pushforward of each assembled member against the metric and wave data at the transported cube offset, and the zero-momentum specialization reduces that to ordinary class dots. Bloch local-incidence identities sum members to recover the full star, the same pattern used for type (1,1).
In the QG campaign this closes the star-kernel step for (1,2) after (1,1); complement orbit (2,1) and other hinge orbits remain open. It does not yet assemble the flat Hessian over all hinges, nor prove continuum EH recovery or flip the gap-action flag. Framework role is discrete gravity infrastructure toward the eight-tick / $D=3$ lattice action, not a direct T0–T8 forcing step.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.