originOffset
plain-language theorem explainer
The origin cube offset on the 4D periodic lattice is the zero translate, encoded as the Fin-3 4-tuple (1,1,1,1). Analysts of the type-(1,3) Regge hinge star cite it as the reference cube that contains the hinge. The body is a four-component constant with decidable Fin membership proofs.
Claim. The origin offset is the 4-tuple $(1,1,1,1)\in(\mathrm{Fin}\,3)^4$, i.e. the candidate unit-cube origin at the lattice origin under the encoding $\{-1,0,1\}\leftrightarrow\{0,1,2\}$.
background
In the type-(1,3) Regge 4D star-kernel module, candidate unit-cube origins on the periodic lattice are points of ${-1,0,1}^4$. They are encoded as CubeOffset $= (\mathrm{Fin},3)^4$, with Fin values $0,1,2$ standing for $-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 module enumerates the full periodic Freudenthal star of the type-(1,3) triangle hinge (absolute masks ${0,1,15}$, local flat squared lengths $(1,3,4)$). Star enumeration needs a distinguished origin cube against which containment of the hinge is decided by finite search over the $3^4$ candidate offsets.
proof idea
Pure definition: the constant 4-tuple of Fin-3 ones, each component proved in range by decide. No lemmas are applied; the term is the origin under the ${-1,0,1}\leftrightarrow{0,1,2}$ encoding.
why it matters
Star enumeration (deliverable A.1 of the module) rests on this constant. Downstream, cubeContainsHinge_origin asserts the origin cube contains the hinge, and only_origin_contains_hinge asserts it is the unique cube among all $3^4$ offsets that does so (both by decide). Those facts pin the six Kuhn simplices of the origin unit cube as the full local star, which then feeds the flat cosine multiset, the $2\pi$ flatness gate, and the 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 does not close that gap.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.