offsetAxis
plain-language theorem explainer
Projects a 4D unit-cube origin offset onto one coordinate axis. Each cube origin is a 4-tuple in {-1,0,1}^4; this returns the Fin-3 code of the chosen axis. Downstream cube-membership tests use it to check hinge vertices axis by axis. The body is a four-clause pattern match on the nested product.
Claim. Given a candidate unit-cube origin $c \in \{-1,0,1\}^4$ (each coordinate coded as an element of $\mathrm{Fin}\,3$) and an axis index $i \in \{0,1,2,3\}$, return the $i$-th coordinate of $c$ as an element of $\mathrm{Fin}\,3$.
background
This module builds the Regge 4D type-(1,3) periodic-lattice star deficit class kernel: the triangle hinge with absolute masks ${0,1,15}$ and its full Freudenthal star in the 4-cube lattice. Deliverable A enumerates which unit cubes contain the hinge and then computes flat cosines, angle sum $2\pi$, and the deficit class kernel on classes $(1,3,5,7,9,11,13)$.
A CubeOffset is a 4-tuple of $\mathrm{Fin},3$ values coding candidate cube origins with each coordinate in ${-1,0,1}$. A hinge vertex with absolute coordinate $v\in{0,1}$ lies in the cube of origin-index $o$ iff $o\le v+1\le o+1$. The four axes are the standard coordinate directions of the 4D lattice.
The hinge itself is the triangle face ${0,1,2}$ of the shared tetrahedron in the glued-pents witness layer; absolute hinge coordinates live in ${0,1}^4$. Axis projection is the first step toward decidable cube-containment of those vertices.
proof idea
Pure definition by pattern match on the nested product encoding of CubeOffset. Axis $0$ returns the first factor, axis $1$ the second, axis $2$ the third, axis $3$ the fourth. No lemmas or tactics; the match is definitional.
why it matters
Feeds vertexInCube, which decides whether a hinge vertex lies in a given cube translate by testing the shifted-interval condition on every axis. That predicate underwrites star enumeration: exactly six Kuhn simplices in the origin cube contain the type-(1,3) hinge, and among cube translates in ${-1,0,1}^4$ only the origin does. Those facts open 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)$. Transport of the kernel to the complementary type $(3,1)$ remains open; this definition is local scaffolding for the (1,3) side only.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.