axisFits
plain-language theorem explainer
Boolean predicate: a cube offset coordinate o ∈ {0,1,2} fits a hinge vertex coordinate v ∈ {0,1} exactly when o−1 ≤ v ≤ o. Used in the type-(1,3) Regge star kernel to decide which lattice cube translates contain a given hinge vertex. Definition is a one-line decidable inequality on Fin values.
Claim. For an axis offset $o \in \{0,1,2\}$ and a hinge absolute coordinate $v \in \{0,1\}$, return true iff $o \le v+1$ and $v+1 \le o+1$ (equivalently $o-1 \le v \le o$).
background
The module builds the full periodic Freudenthal star deficit kernel for the type-(1,3) triangle hinge in 4D Regge calculus on the integer lattice. Absolute hinge masks are ${0,1,15}$ with local flat squared lengths $(1,3,4)$. Star enumeration asks which unit-cube translates in ${-1,0,1}^4$ contain the hinge, and which of the six Kuhn simplices inside the origin cube do so.
Cube offsets are encoded as CubeOffset with per-axis values in Fin 3 (standing for $-1,0,+1$). Hinge vertices carry absolute coordinates in Fin 2 along each of the four axes. Containment of a vertex in a translated cube reduces axiswise to a closed interval test of length one: the offset must place the unit interval over that coordinate.
This predicate is the axiswise atom of that test. It is pure Boolean geometry; no curvature or deficit enters yet.
proof idea
Definition, not a proof. Body is decide on the conjunction $o.val \le v.val+1 \land v.val+1 \le o.val+1$, which Lean discharges by finite enumeration on Fin 3 and Fin 2. Equivalent rewritten form is $o-1 \le v \le o$ on the underlying naturals.
why it matters
Feeds vertexInCube, which lifts the axis test to all four coordinates of a cube offset against a hinge vertex. That in turn supports cubeContainsHinge, the origin-only containment theorem, and the six-simplex star enumeration that underpins the flat cosine multiset, the $2\pi$ flatness gate, and the full-star deficit class kernel on classes $(1,3,5,7,9,11,13)$.
In the QG campaign this is scaffolding for deliverable A of the type-(1,3) kernel: decidable lattice search that only the origin cube contains the hinge. Transport to the complementary type $(3,1)$ remains open; this definition is mask-agnostic and reusable there. It does not touch Einstein–Hilbert recovery or $S_{RS}$ convergence.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.