StarMember
plain-language theorem explainer
Pairs a lattice cube translate with a Kuhn 4-simplex index (0..23) that can contain the type-(1,2) hinge. Downstream star enumeration and deficit-class kernels cite this carrier type. It is a plain product structure with decidable equality; no proof content.
Claim. A star member is a pair $(c,s)$ where $c$ is a cube translate in $\{\mathrm{origin},\,-e_3\}$ and $s\in\{0,\ldots,23\}$ indexes a Freudenthal–Kuhn 4-simplex in the unit hypercube.
background
This module treats the full periodic-lattice star of the type-(1,2) triangle hinge ${0,e_0,e_0+e_1+e_2}$ (masks $0,1,7$) in 4D Regge calculus on the integer lattice. The star lives in two containing unit cubes and four incident 4-simplices.
CubeTranslate is the two-point orbit of cubes that meet this hinge: the origin cube and the cube shifted by $-e_3$. The Freudenthal triangulation of the unit 4-cube yields 24 Kuhn simplices, indexed by Fin 24.
The same pairing pattern appears in the type-(1,1) seed module (four cube translates) and the type-(2,2) corner module; here the cube set is specialized to the (1,2) geometry.
proof idea
No proof: a structure declaration. Fields are the cube translate and the simplex index in Fin 24, with derived DecidableEq and Repr. Instantiation is by anonymous constructors in the starMembers list.
why it matters
Carrier type for deliverable A of the (1,2) star kernel: exact enumeration of the four (cube, simplex) pairs that contain the representative hinge, then flat cosine multiset, $2\pi$ angle sum, and the 15-class deficit kernel with values $\pm\sqrt{2}/2$.
Feeds starMembers in this module and the parallel star-member types in the (1,1) and (2,2) kernels. Sits in the QG full-theory campaign after the (1,1) seed orbit; does not close flat Hessian assembly, $S_{\mathrm{RS}}\to\mathrm{EH}_{4d}$, or gap_action_recovery. Complement type (2,1) remains open.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.