starMembers_complete
plain-language theorem explainer
Exactly six pairs of lattice cube-translate and Kuhn 4-simplex contain the seed triangle hinge; the listed star is complete and has no extras. Gravity analysts assembling the full periodic Freudenthal star deficit cite this as the enumeration gate. The proof is an exhaustive finite case split on the four translates and twenty-four simplices, discharged by decide.
Claim. For every cube translate $c$ among the four lattice shifts $\{\mathrm{origin},-e_2,-e_3,-e_2-e_3\}$ and every Kuhn 4-simplex index $s\in\{0,\ldots,23\}$, the simplex contains the seed hinge under that translate if and only if the pair $(c,s)$ belongs to the enumerated six-member star list.
background
This module is the next kernel-checked increment in the QG full-theory campaign after the dihedral cosine kernel. It treats the seed triangle hinge ${0,e_0,e_0+e_1}$ and its full periodic Freudenthal star in the integer lattice: four containing unit cubes and six incident 4-simplices. Other hinge orbits remain open.
CubeTranslate is the four-element inductive type of lattice shifts that can host the seed hinge (origin, $-e_2$, $-e_3$, $-e_2-e_3$). A pair $(c,s)$ is said to contain the hinge when every local hinge vertex mask of $c$ appears among the five vertex masks of Kuhn simplex $s$ (the Boolean containsHinge). The explicit list starMembers records the six candidate pairs claimed to be exactly those that pass the test.
The surrounding deliverable also records the flat cosine multiset, the $2\pi$ flatness gate, and the full-star deficit class kernel on classes $(2,3,6,7,10,11,14)$. This theorem is only the enumeration half of that package.
proof idea
One-line exhaustive wrapper. Case-split on the four constructors of CubeTranslate, then fin_cases over all twenty-four Kuhn simplex indices, then decide on the resulting Boolean membership statements. No intermediate lemmas are invoked; the finite decidable predicates containsHinge and list membership close every branch.
why it matters
Closes deliverable A.1 (star enumeration) of the Regge 4D full-star deficit class kernel: exactly six (cube translate, Kuhn simplex) pairs contain the seed hinge. Downstream copies in the Kernel12, Kernel13, and Kernel22 modules reuse the same completeness pattern; Kernel13's status flags theorem records starEnumerationClosed = true on the strength of this gate.
In the broader Recognition gravity stack this is a necessary finite check before the flat cosine multiset, the $2\pi$ angle-sum gate, and the signed class kernel $(-1,-1,+1,-1,+1,+1,-1)$ can be trusted. 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 in the module contract.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.