starMembers_length
plain-language theorem explainer
The type-(1,2) Freudenthal star of the representative triangle hinge has exactly four incident (cube translate, Kuhn simplex) pairs. Gravity analysts cite this as the cardinality half of the star-enumeration deliverable for the (1,2) orbit. The proof is definitional: the explicit four-element list reduces by rfl.
Claim. The enumerated list of star members for the type-$(1,2)$ hinge has length $4$.
background
This module is the next kernel-checked increment in the QG full-theory campaign after the type-$(1,1)$ seed orbit. It treats the type-$(1,2)$ triangle hinge ${0, e_0, e_0+e_1+e_2}$ (masks $0,1,7$; difference masks $(1,6)$) and its full periodic Freudenthal star in the integer lattice: two containing unit cubes and four incident 4-simplices.
starMembers is the explicit list of those four pairs: origin with Kuhn indices $0$ and $2$, and the translate minus $e_3$ with indices $18$ and $19$. Length here is ordinary finite-list length (the same primitive used on traces elsewhere in the monolith). Parallel modules record six members for the $(1,1)$ and $(1,3)$ orbits and four again for $(2,2)$.
The module imports the Freudenthal incidence layer, the 15-class stencil, and the committed Gram-projection cosine calculus without redefining their API. Complement type $(2,1)$ remains open and is not transported here.
proof idea
One-line definitional proof. The list literal for starMembers has four constructors, so List.length evaluates to $4$ and rfl closes the equality. No lemmas are invoked beyond the definition of length on a concrete finite list.
why it matters
This is item 1 of deliverable A in the module doc: star enumeration for the $(1,2)$ orbit. Downstream status flags and sibling length theorems in the $(1,1)$, $(1,3)$, and $(2,2)$ kernels reuse the same pattern; the parent star-kernel module and the $(1,3)$ status bundle both depend on having a closed, kernel-checked cardinality.
In the broader Recognition gravity stack this is scaffolding for the full-star deficit class kernel (values $\pm\sqrt{2}/2$ on the 15 stencil classes) and the flatness gate $4\cdot\arccos 0=2\pi$. It does not yet assemble the flat Hessian over all hinges, prove $S_{\mathrm{RS}}$ converges to Einstein–Hilbert in 4D, or flip gap-action recovery. Those remain explicitly open per the module tier tags.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.