only_origin_contains_hinge
plain-language theorem explainer
Among all unit-cube translates with origins in {-1,0,1}^4, only the origin cube contains the type-(1,3) triangle hinge. Gravity and discrete-Regge analysts cite this when closing the Freudenthal star enumeration for the (1,3) kernel. The proof is a pure decidable search over the finite offset set.
Claim. Let cube offsets be 4-tuples with each coordinate in $\{-1,0,1\}$. Among all such offsets, the only cube that contains every vertex of the type-$(1,3)$ hinge is the origin offset. Equivalently, the filtered finite set of hinge-containing offsets equals the singleton $\{\text{origin}\}$.
background
This module is the QG full-theory kernel for the Regge 4D type-(1,3) triangle hinge on the periodic Freudenthal lattice. The hinge has absolute masks ${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)$). The deliverable opens with star enumeration: which Kuhn simplices and which nearby unit cubes meet the hinge.
A cube offset is a candidate origin in ${-1,0,1}^4$, encoded as a 4-tuple of 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. The Boolean cubeContainsHinge is true precisely when all three hinge vertices pass that test for a given offset. The origin offset is the zero translate (encoded $(1,1,1,1)$).
The module already records that exactly six Kuhn simplices in the origin unit cube contain the hinge; the present statement is the complementary global claim that no nontrivial translate in the $3^4$ neighborhood contains it.
proof idea
One-line decidable proof. The ambient type of offsets is finite (Fin 3^4), cubeContainsHinge is a Boolean built from decidable vertex-in-cube checks, and equality of finite sets of Booleans is decidable. Lean closes the identity by decide: exhaustive evaluation shows the filter equals the singleton of the origin offset. No algebraic lemmas are invoked beyond the definitions of the offset type, the origin, and the containment predicate.
why it matters
This is item 1 of deliverable A in the type-(1,3) star-kernel campaign: star enumeration. It pairs with the six-simplex count in the origin cube to pin the full periodic Freudenthal star support. Downstream, hinge4DStarKernel13Status_flags records starEnumerationClosed = true among the kernel status bits, so this theorem is a hard gate on the status board.
In the broader Recognition gravity stack the result is local discrete geometry, not a forcing-chain step (T0–T8) and not an action-recovery claim. The module header is explicit: transport of this kernel to the complementary type (3,1) remains open, flat Hessian assembly over all hinges is open, and neither S_RS_converges_EH_4d nor gap_action_recovery is flipped here. The theorem exists so later cosine, flatness-gate, and full-star deficit-class arguments can assume a unique supporting cube.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.