shiftAxis_dot
plain-language theorem explainer
The covector–basepoint pairing shifts by exactly the a-component when the basepoint is translated one lattice step along axis a: m·(x+e_a)=m·x+m_a on the 4-torus. Anyone tracking plane-wave phases or discrete Lie loadings on axis edges cites this. The proof unfolds the coordinatewise shift, splits the sum, and collapses the indicator via Finset.sum_ite_eq'.
Claim. For covector $m\in\mathbb{R}^4$, basepoint $x\in\mathbb{R}^4$, and axis $a\in\{0,1,2,3\}$, if $x+e_a$ denotes the covering-space shift of $x$ by one lattice step along axis $a$, then $\sum_{i=0}^{3} m_i(x+e_a)_i=\sum_{i=0}^{3} m_i x_i+m_a$.
background
This module is the plane-wave attachment layer for 4D Regge edge TT analysis (QG Wave 4 / W4-1). It sits on top of the algebraic Euclidean $4\times 4$ TT/gauge/transverse-trace split and loads those pieces onto axis edges of the 4-torus, using the same quadratic-form convention as the 3D chain.
The covering-space shift shiftAxis x a is the map $i\mapsto x_i+1$ on coordinate $a$ and $x_i$ elsewhere: one lattice step along axis $a$. Plane-wave phases are linear pairings $\theta=m\cdot x=\sum_i m_i x_i$; midpoint phases on axis edges add the half-step $m_a/2$. Discrete Lie loadings of squared axis-edge length from a vertex field compare the field at $x+e_a$ and at $x$, so the phase (and the pairing) must transform under that shift.
The identity here is the elementary finite-difference fact that the pairing picks up exactly $m_a$ under that unit step.
proof idea
Unfold the definition of the axis shift so each summand is $m_i$ times an if-then-else on $i=a$. For each $i$, rewrite $m_i\cdot(\text{if }i=a\text{ then }x_i+1\text{ else }x_i)$ as $m_i x_i$ plus $m_i$ times the corresponding $0/1$ indicator (split_ifs and ring). Sum-add distributivity separates the original pairing from the indicator sum; Finset.sum_ite_eq' collapses the indicator sum to the single term $m_a$.
why it matters
Feeds discreteLieAxis_eq, the exact trig expansion of the discrete Lie loading on an axis edge: $2(\xi_a(x+e_a)-\xi_a(x))$ for the plane-wave vertex field $\xi_b(x)=v_b\sin(m\cdot x)$. That expansion needs the shifted phase $m\cdot(x+e_a)=m\cdot x+m_a$ to produce the factor $2v_a\cdot\mathrm{latticeDerivSymbol}(m,a)\cdot\cos(\text{midpoint phase})$.
In the module's honest scope this is the lattice identity linking matrix-gauge edge loadings of gaugePart to discrete Lie loadings (with the sinc prefactor $m_a/(2\sin(m_a/2))$ when $\sin(m_a/2)\neq 0$). It is not the continuum claim $\delta\ell^2=2\partial_a\xi_a$, nor full 4D Regge action recovery or $S_{\mathrm{RS}}\to\mathrm{EH}_{4d}$. It is a small but necessary phase bookkeeping step in the gauge $\leftrightarrow$ discrete-Lie bridge of the edge-TT attachment campaign.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.