starSlotClass
plain-language theorem explainer
Lookup table sending each of six star members and ten local edge slots to a global edge class in the 15-class stencil, for the type-(1,3) Regge hinge after hinge-ordered vertex reordering. Anyone assembling the full-star deficit kernel cites it. The body is an exhaustive case table fixed by the Freudenthal chain on apexes.
Claim. For each star member $m\in\{0,\ldots,5\}$ and each local edge slot $e\in\{0,\ldots,9\}$, return the global edge class in $\{0,\ldots,14\}$ obtained after reordering vertices so the hinge is $(0,1,15)$ and the apexes follow the Freudenthal chain.
background
This module builds the Regge 4D type-(1,3) periodic-lattice star deficit class kernel. The hinge has absolute masks ${0,1,15}$ (difference masks $(1,14)$, local flat squared lengths $(1,3,4)$). Exactly six Kuhn simplices in the origin unit cube contain that hinge; their flat cosines are all $1/2$, so the star angle sum is $2\pi$.
Edges of the 4-simplex are bucketed into a fixed 15-class stencil used by the Gram-projection cosine calculus and the cleared-denominator master lemma at flat values $(N,P,Q)=(8,8,8)$. Sister kernels for type $(1,1)$ and other orbits define analogous slot-to-class maps; this table is the type-(1,3) instance after the same hinge-first reordering.
Local slots run over the ten edges of one simplex; star members index the six simplices of the full periodic Freudenthal star.
proof idea
Pure definition by exhaustive pattern match: sixty concrete assignments $(m,e)\mapsto c\in\mathrm{Fin},15$. No lemmas, no tactics. The values encode the incidence of each local edge, after vertices are ordered so the hinge is $(0,1,15)$ and apexes follow the Freudenthal chain, into the global 15-class stencil already fixed by the edge-stencil layer.
why it matters
This table is the wiring that lets assembleStarMember push local deficit kernel values onto global classes: for each member $m$ one sums, over local slots $e$, the local kernel entry whenever the slot class equals the target class $d$. Downstream member-evaluation lemmas (member2_eval through member5_eval and siblings) unfold that assembly and obtain the sparse support used to build the full-star deficit class kernel 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})$.
It is deliverable A item 5 of the type-(1,3) campaign: without a correct slot-to-class map the flatness gate, coordinate derivatives, and stationarity gates cannot be stated on the global stencil. Transport of the same kernel to the complementary type $(3,1)$ remains open; this definition does not address that transport.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.