CubeOffset
plain-language theorem explainer
Type of candidate unit-cube origins on the 4D periodic lattice, each coordinate drawn from {-1,0,1} and encoded as Fin 3. Used throughout the type-(1,3) Regge hinge star kernel to enumerate which translated cubes can contain the hinge. Pure type synonym; no proof content.
Claim. Write $\mathrm{CubeOffset} := (\mathbb{F}_3)^4$, the set of 4-tuples with each entry in $\{0,1,2\}$, standing for candidate unit-cube origins whose coordinates lie in $\{-1,0,1\}$.
background
This module is the next kernel-checked increment in the QG full-theory campaign for Regge calculus in 4D: the type-(1,3) triangle hinge with absolute masks ${0,1,15}$ and its full periodic Freudenthal star. It imports the incidence layer, the 15-class stencil, and the Gram-projection cosine calculus without redefining their API.
A cube offset indexes a translate of the origin unit cube by a vector in ${-1,0,1}^4$. Encoding each coordinate as an element of $\mathrm{Fin},3$ (values $0,1,2$) makes the finite search space decidable. The doc-comment records the membership test: 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$.
Downstream predicates (vertexInCube, cubeContainsHinge) and the origin representative are built directly on this type.
proof idea
Definitional abbreviation only: a four-fold product of Fin 3. No tactics, no lemmas, no computational content beyond the type former.
why it matters
Anchors the star-enumeration deliverable of the type-(1,3) kernel. Every cube-membership predicate and the two decidable theorems that pin the star geometry (star_cube_cardinality, only_origin_contains_hinge) quantify over this type. Those results establish that exactly one cube translate in ${-1,0,1}^4$ contains the hinge (the origin), which is the first item in the module's proved list and the gate before flat-cosine multisets, the $2\pi$ flatness gate, and the full-star deficit class kernel on classes $(1,3,5,7,9,11,13)$.
Does not itself touch Einstein–Hilbert recovery or gap-action; it is scaffolding for the local lattice search that those later gates rely on. Transport of the same kernel to the complementary type $(3,1)$ remains open.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.