starSlotClass
plain-language theorem explainer
Lookup that sends each of the six star 4-simplices and each of its ten local edge slots to one of the fifteen global edge classes on the periodic lattice stencil. Anyone assembling the full-star deficit class kernel cites it. Pure definition: members 0–1 delegate to the flat-kernel local edge class map; members 2–5 are explicit tables.
Claim. For each star member $m\in\{0,\ldots,5\}$ and local edge slot $e\in\{0,\ldots,9\}$, return the global edge class in $\{0,\ldots,14\}$ of that edge after hinge-ordered placement. Members $m=0,1$ reuse the flat-kernel local edge class of simplices $0$ and $1$; members $m=2,3,4,5$ are given by fixed tables (e.g. member $2$ sends slots $(0,\ldots,9)$ to classes $(0,2,3,10,1,4,9,6,7,14)$).
background
The module builds the full periodic-lattice star deficit class kernel for the seed triangle hinge ${0,e_0,e_0+e_1}$ in the 4D Freudenthal triangulation. Exactly six (cube translate, Kuhn simplex) pairs contain that hinge; each 4-simplex has ten edges, and the lattice edge orbits are partitioned into fifteen global classes via the imported 15-class stencil.
Upstream, localEdgeClass (from the flat kernel) already maps a simplex index and local slot to a class in $\mathrm{Fin},15$ by reading the local edge mask. Sibling star kernels (12, 13, 22) define analogous slot-to-class tables for smaller or reordered star subsets. Here the six star members are indexed in starMembers order, with vertices reordered so the hinge is fixed and apexes follow the Freudenthal chain.
The map is the incidence bookkeeping layer: it does not compute angles or deficits, only which global class each local edge belongs to.
proof idea
Definition by cases, no proof obligations. On star members $0$ and $1$ it is a one-line wrapper around the flat-kernel local edge class map for simplices $0$ and $1$. On members $2$–$5$ it is an exhaustive pattern match on the ten local slots, each clause a constant in $\mathrm{Fin},15$. The tables encode the hinge-ordered embedding of those four simplices into the global stencil.
why it matters
This is the incidence spine of deliverable A in the module doc: the full-star deficit class kernel on classes $(2,3,6,7,10,11,14)$. Downstream, assembleStarMember folds the local deficit kernel over slots by summing only those $e$ with matching class, and the private member2_eval–member5_eval lemmas evaluate that sum to sparse class-supported rationals (halves and quarters).
Those assemblies feed the star-level gates (flat angle sum $2\pi$, nonvacuity, swap-$2\leftrightarrow 3$ symmetry, uniform-scaling decoy, homothety stationarity). In the QG campaign this is the next kernel-checked increment after the dihedral cosine kernel; it does not yet close flat Hessian assembly over all hinges, nor $S_{\mathrm{RS}}\to\mathrm{EH}_{4d}$, nor gap_action_recovery. It sits in the gravity analysis stack that eventually supports continuum recovery of Einstein–Hilbert from the Recognition action on the lattice.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.