shiftAxis
plain-language theorem explainer
Covering-space shift of a 4-torus basepoint by one lattice step along a chosen axis. Anyone building discrete Lie loadings or midpoint phases on axis edges cites it. The body is a one-line coordinate bump: add 1 on the selected axis index and leave the other three coordinates fixed.
Claim. For a basepoint $x \in \mathbb{R}^4$ and axis index $a \in \{0,1,2,3\}$, define the lattice translate $(T_a x)_i = x_i + \delta_{ia}$. Equivalently, $T_a x = x + e_a$ on the integer covering space of the 4-torus.
background
This module sits in the QG full-theory campaign (Wave 4 / lane W4-1): attach the Euclidean $4\times 4$ TT / gauge / transverse-trace split to plane-wave edge loadings on axis edges of the 4-torus. The quadratic-form convention matches the 3D chain: edge load of a matrix $H$ along displacement $D$ is $\sum_{ij} H_{ij} D^i D^j$.
Axis edges are the four coordinate directions $e_a$. Gauge vertex fields are of the form $\xi_b(x) = v_b \sin(m\cdot x)$. Comparing $\xi$ at $x$ and at the neighboring lattice point requires a pure lattice translate along one axis; that translate is exactly this shift.
The surrounding layer proves linearity of edge load, transport of the TT decomposition onto plane-wave edge perturbations, and an exact finite-difference identity relating matrix-gauge edge load to discrete Lie loading (not the continuum claim $\delta\ell^2 = 2\partial_a\xi_a$).
proof idea
Pure definitional term: the function that returns $x_i+1$ when $i=a$ and $x_i$ otherwise. No lemmas, no tactics. Downstream proofs unfold it and case-split on the axis index (as in the companion identity for the covector dot product after the shift).
why it matters
This is the geometric primitive behind discrete Lie loading on axis edges. discreteLieAxis is defined as $2(\xi_a(T_a x)-\xi_a(x))$, the first-order change of squared axis-edge length under a vertex displacement field. The exact trig expansion discreteLieAxis_eq and the phase identity shiftAxis_dot both depend on it: after the shift, $m\cdot(T_a x)=m\cdot x+m_a$, which produces the midpoint phase $m\cdot x+m_a/2$ and the lattice derivative symbol $2\sin(m_a/2)$.
In the module's honest scope, that identity equates the matrix-gauge plane-wave edge perturbation to $(m_a/(2\sin(m_a/2)))$ times the discrete Lie loading whenever $\sin(m_a/2)\neq 0$. The shift itself is scaffolding for that lattice gauge story; it does not touch continuum Einstein-Hilbert recovery or the ledger name edge_tt_decomposition in full.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.