vertexInCube
plain-language theorem explainer
Boolean predicate: a type-(1,3) hinge vertex lies in a candidate unit cube whose origin sits in {-1,0,1}^4. Star-enumeration proofs cite it when filtering Freudenthal cubes that meet the hinge. The body is a four-axis conjunction of the shifted interval test, discharged by decide.
Claim. For a cube origin $c\in\{-1,0,1\}^4$ and hinge-vertex index $k\in\{0,1,2\}$, return true iff every coordinate axis $i=0,\ldots,3$ satisfies the shifted interval test $o_i\le v_{k,i}+1\le o_i+1$, where $o_i$ is the $i$-th component of $c$ and $v_{k,i}\in\{0,1\}$ is the absolute hinge coordinate of vertex $k$ on axis $i$.
background
Module setting: the Regge 4D type-(1,3) periodic-lattice star deficit kernel. Scope is the triangle hinge with absolute masks ${0,e_0,e_0+e_1+e_2+e_3}={0,1,15}$ and its full periodic Freudenthal star; complementary type (3,1) transport remains open.
CubeOffset encodes candidate unit-cube origins with each coordinate in ${-1,0,1}$ as a 4-tuple of Fin 3. offsetAxis projects that tuple onto a single spacetime axis. absHingeCoord supplies the three hinge vertices as points in ${0,1}^4$ (vertex 0 is the origin; vertex 1 is $e_0$; vertex 2 is the all-ones vector). axisFits o v is the Boolean for the shifted containment $o\le v+1\le o+1$.
Together these pieces decide, axis by axis, whether a named hinge vertex sits inside a translated unit cube. That is the atomic containment test used by the star-enumeration deliverable (exactly six Kuhn simplices in the origin cube contain the hinge; among ${-1,0,1}^4$ translates only the origin does).
proof idea
Definition, not a theorem. Body is decide on the universal quantifier over the four axes: for each $i:\mathrm{Fin},4$, evaluate axisFits on (offsetAxis c i, absHingeCoord k i) and require the result to be true. No lemmas are applied; the Boolean is pure finite arithmetic on Fin values.
why it matters
Feeds cubeContainsHinge, which folds this predicate over all three hinge vertices and is the filter in the star-enumeration campaign: six Kuhn simplices contain the hinge at the origin, and only the origin cube among ${-1,0,1}^4$ translates does. That enumeration is deliverable A.1 of the type-(1,3) kernel module, upstream of the flat cosine multiset, the $2\pi$ flatness gate, the ten coordinate derivatives at $(N,P,Q)=(8,8,8)$, and the full-star deficit class kernel on classes $(1,3,5,7,9,11,13)$.
In the broader QG campaign this is scaffolding for the Freudenthal incidence layer after the type-(1,1) seed orbit; it does not yet assemble the flat Hessian over all hinges, prove $S_{\mathrm{RS}}$ converges to EH in 4D, or flip gap_action_recovery.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.