starMembers
plain-language theorem explainer
Explicit four-element roster of Freudenthal star members for the type-(2,2) triangle hinge on the 4D periodic lattice: only the origin cube corner, paired with Kuhn simplices 0, 1, 6, and 7. Gravity analysts building the Regge deficit-class kernel cite this as the ground-truth incidence list. The body is a pure list literal, not a filtered computation.
Claim. The star of the type-$(2,2)$ hinge $\{0, e_0+e_1, e_0+e_1+e_2+e_3\}$ on the 4D Freudenthal lattice consists of exactly four members: the origin cube corner paired with Kuhn simplex indices $s \in \{0,1,6,7\}$.
background
This module treats the type-(2,2) triangle hinge orbit in 4D Regge calculus on the periodic Freudenthal triangulation. The hinge is the triangle with vertex masks ${0,3,15}$ (difference masks $(3,12)$). A star member is a pair of an axis-aligned unit-cube corner (coordinates in ${-1,0}$) and a Kuhn simplex index in $\mathrm{Fin},24$ that contains that hinge.
Sibling structure StarMember packages those two fields. Upstream kernels for orbits (1,1) and (1,2) use analogous lists, but with multiple cube translates and different simplex indices; the (1,3) kernel collapses to simplex indices alone. Here the geometry forces a single corner (the origin) and four simplices.
The module imports the dihedral and flat kernels plus the 15-class edge stencil; it never redefines their API. Scope is the full periodic star of this one hinge orbit only.
proof idea
Pure definition by enumeration: the body is the four-element list literal of pairs (cube corner 0, simplex $s$) for $s \in {0,1,6,7}$. No tactics, no lemmas, no filtering. Completeness and cardinality are discharged later by separate decide-style theorems that case-split over corners and simplices against the containment predicate.
why it matters
Delivers item 1 of the module's deliverable A (star enumeration): exactly four (cube, simplex) pairs contain the (2,2) hinge, and only the origin among the 16 candidate corners does so. Downstream theorems starMembers_length, starMembers_complete, and star_cardinality quote this list as the reference set; sibling kernels for other orbits mirror the same pattern.
It feeds the flat-cosine multiset, the $2\pi$ angle-sum flatness gate, and the full-star deficit-class kernel on all 15 stencil classes. In the Recognition Science gravity campaign this is the next kernel-checked increment after the (1,1) seed orbit toward assembling the 4D Regge action; it does not yet close Hessian assembly, $S_{\mathrm{RS}}\to\mathrm{EH}_{4d}$, or gap-action recovery. Bloch local-incidence code also consumes star-member geometry when translating cubes to $\mathbb{R}^4$ offsets.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.