CubeTranslate
plain-language theorem explainer
Four-valued label set for the unit-cube lattice translates that can contain the seed triangle hinge in the 4D Freudenthal star. Gravity analysts cite it when indexing the six incident 4-simplices or writing cube offsets in ℝ⁴. The declaration is a plain inductive enumeration with decidable equality and a Fintype instance; no proof content.
Claim. A finite type with four constructors labeling the integer-lattice translates of the unit 4-cube that participate in the full periodic star of the seed hinge $\{0,e_0,e_0+e_1\}$: the origin cube, the cube shifted by $-e_2$, the cube shifted by $-e_3$, and the cube shifted by $-e_2-e_3$.
background
The module builds the full-star deficit class kernel for Regge calculus on the 4D integer lattice after the dihedral-cosine seed kernel. The local setting is the seed triangle hinge ${0,e_0,e_0+e_1}$ and its periodic Freudenthal star: four containing unit cubes and six incident 4-simplices. Other hinge orbits remain open.
A cube translate is the discrete offset that places a unit cube relative to that seed. The four values match the geometry of the star: only shifts in the $e_2$ and $e_3$ directions (the two directions transverse to the hinge plane) can still contain the hinge. An earlier two-constructor version in the type-(1,2) kernel is the direct upstream ancestor; this four-constructor form is the committed type-(1,1) enumeration.
Downstream code turns each label into an $\mathbb{R}^4$ offset vector and into Boolean hinge-containment tests against Kuhn simplex masks.
proof idea
Definitional inductive type, not a proved statement. Four nullary constructors, with derived DecidableEq, Repr, and Fintype. No tactics, no lemmas applied. Pattern-matching on the constructors is the intended use site.
why it matters
This label set is the indexing spine of deliverable A in the module doc: star enumeration of exactly six (cube translate, Kuhn simplex) pairs. Downstream, cubeOffsetT11 and cubeTranslateOffset map each constructor to an $\mathbb{R}^4$ lattice offset; starMemberCubeT11 assigns cubes to the six star members; containsHinge and localHingeMasks decide which simplices sit in which cube. Those feed the flat-cosine multiset, the $2\pi$ flatness gate, and the full-star deficit class kernel on classes $(2,3,6,7,10,11,14)$.
In the QG campaign this is infrastructure only: it does not assemble the flat Hessian over all hinges, does not prove $S_{\mathrm{RS}}$ converges to Einstein–Hilbert in 4D, and does not flip gap_action_recovery. It is the discrete bookkeeping step that makes the six-simplex star finite and machine-checkable.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.