starMembers_complete
plain-language theorem explainer
A Kuhn simplex index in the 24-cell origin cube contains the type-(1,3) Regge triangle hinge exactly when it lies in the fixed star-member list. Gravity analysts building the 4D deficit class kernel cite this to lock star support before cosine and derivative work. The proof is exhaustive case split on Fin 24 followed by decidable Boolean evaluation.
Claim. For every Kuhn simplex index $s\in\{0,\ldots,23\}$, the Boolean predicate "simplex $s$ contains the type-$(1,3)$ hinge" holds if and only if $s$ belongs to the enumerated star-member list of the origin unit cube.
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,3) triangle hinge whose absolute masks are ${0,e_0,e_0+e_1+e_2+e_3}={0,1,15}$ (difference masks $(1,14)$, local flat squared lengths $(1,3,4)$) and its full periodic Freudenthal star inside the 4D unit-cube Kuhn triangulation.
The local predicate containsHinge decides whether every mask of the hinge appears among the five vertex masks of a given simplex. The list starMembers is the explicit enumeration of those simplices that pass the test. Upstream type-(1,1) and type-(1,2) kernels prove the analogous biconditional over cube translates; here the statement is specialized to the origin cube (Fin 24 only), matching the module claim that exactly six Kuhn simplices contain the hinge and only the origin translate does so among ${-1,0,1}^4$.
The surrounding layer imports the Freudenthal incidence API, the 15-class edge stencil, and the Gram-projection cosine calculus without redefining them.
proof idea
One-line wrapper. fin_cases s splits on all 24 simplex indices; each goal is closed by decide on the decidable Boolean equality containsHinge s = true versus list membership. No algebraic lemmas are invoked; the proof is pure finite exhaustive search.
why it matters
Locks deliverable A item 1 of the module: star enumeration for the type-(1,3) hinge. Downstream, hinge4DStarKernel13Status_flags records starEnumerationClosed = true by citing this theorem, which in turn gates the flatness check ($6\cdot\arccos(1/2)=2\pi$), the ten coordinate derivatives at flat values $(N,P,Q)=(8,8,8)$, and the full-star deficit class kernel on classes $(1,3,5,7,9,11,13)$ with values $(-\sqrt{3},-\sqrt{3},+\sqrt{3},-\sqrt{3},+\sqrt{3},+\sqrt{3},-\sqrt{3})$.
Sibling completeness theorems in the type-(1,1), (1,2) and (2,2) kernels form the same pattern; this instance fills the (1,3) slot. It does not transport the kernel to the complementary type (3,1) (explicitly left OPEN) and does not assemble the flat Hessian over all hinges or flip gap_action_recovery / S_RS_converges_EH_4d.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.