cubeOffsetT12
plain-language theorem explainer
Assigns lattice offset vectors to the two cubes in a type-(1,2) 4D Regge star: origin maps to the zero wave, and the cube shifted by −e₃ maps to the wave with −1 in coordinate 3. Gravity analysts cite it when building position-resolved deficit phases for the exact flat cross-term Hessian. The body is a two-clause pattern match on the CubeTranslate inductive.
Claim. The lattice translate of a type-$(1,2)$ star cube is the map $T_{(1,2)}$ from the two-element cube-translate set $\{\mathrm{origin},\,-e_3\}$ into waves $\mathbb{R}^4$ with $T_{(1,2)}(\mathrm{origin})=0$ and $T_{(1,2)}(-e_3)=(-\delta_{i3})_{i=0}^{3}$.
background
This module builds the exact flat cross-term continuum symbol of the 4D Regge action Hessian on the Freudenthal torus (oracle tag H_fold). At flat background, deficits vanish, so Schläfli reduces the second variation to the cross term $S''=\sum_h (dA_h)(d\delta_h)$. Plane-wave class strains need position-resolved deficit phasing: type-(1,1) keeps full star-member cube offsets, while type-(1,2) uses a thinner cube set.
Wave4 is simply $\mathrm{Fin},4\to\mathbb{R}$, a four-component real wave (or lattice displacement). The upstream inductive CubeTranslate in the type-(1,2) star kernel has only two constructors, origin and minusE3, reflecting the reduced geometry of a (1,2) hinge star versus the four-cube (1,1) star (origin, minusE2, minusE3, minusE2E3).
The offset is the lattice vector by which that star-member cube is translated relative to the hinge origin; it enters the phase factor when the deficit is evaluated on a Bloch wave at a transported basepoint.
proof idea
Pure definition by cases on the two constructors of the type-(1,2) CubeTranslate inductive. The origin clause returns the zero wave. The minusE3 clause returns the standard basis wave with value $-1$ in slot $i=3$ and $0$ elsewhere. No lemmas are invoked.
why it matters
Supplies the cube-offset data that phasedDeficitDotResolvedT12 folds into the transported basepoint of each star member: the wave argument is $x_i + \mathrm{transportOffset},p,(T_{(1,2)}(\mathrm{cube}(\mu)))_i$. The zero-momentum specialization phasedDeficitDotResolvedT12_zeroMomentum inherits the same offset table.
In the H_fold program this is bookkeeping for the geometry-derived flat cross-term (MODEL tier exactFlatCrossTermFold / finiteExactReggeSymbol), not yet the full Schläfli lift from nonlinear $S$. It is the (1,2) twin of the sibling offset for type (1,1). Open items upstream of this def (ContinuumSymbolIs Tendsto, ledger $S_{RS}$, e0 isotropy) are unaffected; the def only fixes the discrete phase origin for (1,2) hinges.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.