cubeContainsHinge
plain-language theorem explainer
Boolean test: a lattice cube offset contains the type-(1,3) triangle hinge exactly when all three hinge vertices sit in that unit cube. Star-enumeration theorems cite it to pin the hinge to the origin among the 3^4 candidate translates in {-1,0,1}^4. The body is a one-line decidable universal check over the three vertices.
Claim. For a candidate unit-cube origin $c \in \{-1,0,1\}^4$, return true if and only if every vertex of the type-$(1,3)$ triangle hinge lies in the unit cube with that origin.
background
This module builds the Regge 4D type-(1,3) periodic-lattice star deficit class kernel: the triangle hinge with absolute masks ${0, e_0, e_0+e_1+e_2+e_3}={0,1,15}$ and its full Freudenthal star. Deliverable A opens with star enumeration among Kuhn simplices and cube translates.
A CubeOffset is a 4-tuple of coordinates in ${-1,0,1}$, encoded as Fin 3 values. A hinge vertex with absolute coordinate $v\in{0,1}$ lies in the cube of origin-index $o$ iff the shifted interval test $o \le v+1 \le o+1$ holds on every axis. The sibling predicate vertexInCube packages that axis-wise fit for one of the three hinge vertices.
cubeContainsHinge lifts the per-vertex test to the whole hinge: the cube contains the hinge when all three vertices pass.
proof idea
Definition, not a proof. Body is decide of the universal statement that every hinge vertex index $k:\mathrm{Fin},3$ satisfies the Boolean vertexInCube test for the given offset. Lean discharges the decision procedure from the finite product structure of offsets and axes; no lemmas are applied beyond that decidability.
why it matters
Local gate for the star-enumeration half of deliverable A in the type-(1,3) kernel. Downstream, cubeContainsHinge_origin shows the origin offset returns true; only_origin_contains_hinge shows the filtered set of containing offsets equals the singleton origin; star_cube_cardinality records that the filtered cardinality is 1. Those facts underwrite the claim that among cube translates in ${-1,0,1}^4$ only the origin contains the hinge, which is the lattice half of "exactly six Kuhn simplices in the origin unit cube contain the hinge."
The module does not yet transport the kernel to the complementary type (3,1), nor complete flat Hessian assembly or $S_{RS}\to EH$ convergence. This predicate is pure scaffolding for the decidable search that closes the origin-uniqueness step.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.