cubeOffsetT11
plain-language theorem explainer
Assigns to each of the four lattice translates of a type-(1,1) star cube its displacement 4-vector on the Freudenthal lattice: origin to zero, and the three nonzero translates to −e₂, −e₃, and −e₂−e₃. Downstream resolved deficit contractions cite it to place star-member cubes before plane-wave phasing. Pure case split on the CubeTranslate inductive; no proof content.
Claim. Map each lattice translate $t$ of a type-$(1,1)$ star cube to a displacement $v_t\in\mathbb{R}^4$ by $v_{\mathrm{origin}}=0$, $v_{-e_2}=-e_2$, $v_{-e_3}=-e_3$, and $v_{-e_2-e_3}=-e_2-e_3$ (components indexed by $\mathrm{Fin}\,4$).
background
The module builds the exact flat cross-term continuum symbol of the Regge action Hessian on the Freudenthal torus. At flat background, deficits vanish and Schläfli reduces the second variation to the cross term $S''=\sum_h (dA_h)(d\delta_h)$. Type-$(1,1)$ hinges keep star-member cube offsets for position-resolved deficit phasing; other hinge types use per-edge transported origins.
Wave4 is simply $\mathrm{Fin},4\to\mathbb{R}$, a real 4-vector (wave covector or lattice offset). Upstream CubeTranslate (from the type-$(1,1)$ star-kernel module) is the four-point inductive of cube positions relative to a hinge star: origin, $-e_2$, $-e_3$, and $-e_2-e_3$. A parallel, smaller inductive exists for type-$(1,2)$ stars.
These offsets feed the Bloch/plane-wave bookkeeping that distinguishes the true continuum object from the mis-transported fold blochFoldAllDistinctHinge.
proof idea
Definition by exhaustive pattern match on CubeTranslate. Origin maps to the zero 4-vector. The three nonzero constructors each set the indicated coordinate(s) of $\mathrm{Fin},4$ to $-1$ and the rest to $0$, yielding $-e_2$, $-e_3$, and $-e_2-e_3$. No lemmas or tactics.
why it matters
Local bookkeeping for the $H_{\mathrm{fold}}$ pivot: the true Regge Hessian on the Freudenthal torus should annihilate vertex-gauge modes and send normalized TT on axisTTPlus/symbolDir to $-1/4$. Type-$(1,1)$ resolved deficits need star-member cubes placed at their lattice translates before cosine phasing.
Parent uses: phasedDeficitDotResolvedT11 sums star members at offsets transportOffset p (cubeOffsetT11 (starMemberCubeT11 μ)); the zero-momentum theorem then drops phases and recovers ordinary class dots. That contraction is the type-$(1,1)$ piece of the geometry-derived flat cross-term model (exactFlatCrossTermFold / finiteExactReggeSymbol). Open items upstream of this def (Tendsto continuum symbol, ledger $S_{RS}$) are unaffected; the def only fixes discrete cube placement.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.