cubeContainsHinge_origin
plain-language theorem explainer
The origin unit-cube translate on the 4D periodic lattice contains every vertex of the type-(1,3) triangle hinge. Star-enumeration arguments in the Regge deficit kernel cite this as the reference containment fact. The proof is a pure decidability check on the three hinge vertices.
Claim. For the origin cube offset on the 4D lattice, the Boolean predicate that every vertex of the type-$(1,3)$ triangle hinge lies in that cube evaluates to true.
background
This module builds the type-$(1,3)$ full-star deficit class kernel for 4D Regge calculus on the periodic Freudenthal lattice. The hinge is the triangle with 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)$). Cube offsets are lattice translates; the origin offset is the reference unit cube.
Containment of a hinge in a cube is the Boolean that all three hinge vertices lie inside that cube translate (checked coordinatewise via the vertex-in-cube predicate). The star-enumeration deliverable asserts that exactly six Kuhn simplices in the origin cube meet the hinge, and that among translates in ${-1,0,1}^4$ only the origin cube contains it.
The local setting is kernel-checked geometry only: no Hessian assembly, no Einstein–Hilbert weight reverse-engineering, and no claim that the RS action converges to EH in 4D.
proof idea
One-line decidable proof. Unfold containment to the finite universal check that each of the three hinge vertices lies in the origin cube, then discharge by decide on the Boolean equality to true. No algebraic lemmas beyond the definitions of the origin offset and the containment predicate.
why it matters
This is the base case of deliverable A (star enumeration) in the type-$(1,3)$ kernel: the hinge sits in the reference cube before counting the six Kuhn simplices and proving uniqueness among nearby translates. Downstream, the status theorem hinge4DStarKernel13Status_flags records starEnumerationClosed = true among the kernel gates.
In the QG campaign this sits after the type-$(1,1)$ seed-orbit kernel and the orbit classification layer. It does not close type-$(3,1)$ transport (explicitly open by mask complement), flat Hessian assembly, gap-action recovery, or $S_{\mathrm{RS}}\to\mathrm{EH}_{4d}$. It is pure lattice incidence scaffolding for the later flat-cosine multiset, $2\pi$ flatness gate, and the seven-class deficit kernel values $(\pm\sqrt{3})$.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.