starMembers
plain-language theorem explainer
Enumerates the six Kuhn simplices (indices 0–5 in Fin 24) that form the periodic Freudenthal star of the type-(1,3) triangle hinge at the origin cube. Gravity analysts cite it when building the flat cosine multiset, angle-sum gate, and deficit class kernel for that orbit. It is a literal list constant, fixed by the prior star-cardinality and origin-only search.
Claim. The star of the type-$(1,3)$ Regge triangle hinge (absolute masks $\{0,1,15\}$) is the list of Kuhn simplex indices $0,1,2,3,4,5$ in $\mathrm{Fin}\,24$, all lying in the origin unit cube.
background
In the 4D Regge campaign the spatial lattice is the Freudenthal–Kuhn triangulation of the unit hypercube into 24 ordered simplices. A triangle hinge is typed by its edge-length signature; type $(1,3)$ has absolute vertex masks ${0,e_0,e_0+e_1+e_2+e_3}={0,1,15}$ and local flat squared lengths $(1,3,4)$.
The star of a hinge is the set of Kuhn simplices that contain it. Module scope restricts attention to cube translates in ${-1,0,1}^4$. Sibling facts already show that exactly six simplices of the origin cube contain the hinge and that no non-origin translate in the window does.
Upstream kernels for types $(1,1)$ and $(1,2)$ store star members as pairs (cube translate, simplex index). For type $(1,3)$ the translate is always the origin, so the star collapses to a plain list of six indices in $\mathrm{Fin},24$.
proof idea
Pure definition: the constant list literal $[0,1,2,3,4,5]$ of type $\mathrm{List},(\mathrm{Fin},24)$. No tactic or lemma application; completeness and length are discharged by the companion theorems that case-split on cube translates and run decide.
why it matters
First deliverable of the type-$(1,3)$ star-deficit kernel. Downstream starMembers_complete and starMembers_length certify that the list is exhaustive and has cardinality 6, unlocking the shared Gram vector (all six flat cosines equal $1/2$), the flatness gate $6\cdot\arccos(1/2)=2\pi$, and the full-star deficit class values on classes $(1,3,5,7,9,11,13)$. Parallel star-member lists in the $(1,1)$, $(1,2)$ and $(2,2)$ kernels reuse the same naming pattern so the Bloch incidence and Hessian assembly layers can treat orbits uniformly. Transport of the kernel to the complementary type $(3,1)$ remains open; the list itself does not close flat-Hessian assembly or $S_{\mathrm{RS}}\to\mathrm{EH}$ convergence.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.