fst_add_e2
plain-language theorem explainer
Shifting a 3D lattice site by the z-axis unit vector leaves the x-coordinate unchanged. Downstream axis-sector Laplacian and transversality proofs cite this as a simp fact when evaluating stencils on modes constant in y and z. The proof is a one-line appeal to integer add-zero on the first factor.
Claim. For every lattice site $x = (x_1,x_2,x_3)\in\mathbb{Z}^3$, the first coordinate of $x + e_2$ equals $x_1$, where $e_2 = (0,0,1)$ is the unit step along the third axis.
background
The module builds the discrete Lichnerowicz operator on the flat 3-torus as part of Seven-Gaps Lane 4 (operator convergence). Lattice sites are Site3 := ℤ × ℤ × ℤ, with the periodic interpretation of the unit 3-torus; fields are N-periodic functions on ℤ rather than on ZMod N, so stencil identities hold pointwise.
unitVec : Fin 3 → Site3 supplies the three axis steps: index 0 is (1,0,0), index 1 is (0,1,0), and index 2 is (0,0,1). Adding unitVec 2 therefore increments only the third coordinate. Component projections of such shifts are elementary arithmetic facts needed when the 3D discrete Laplacian or discrete divergence is expanded along each axis.
All convergence results in the file are restricted to the axis stencil sector (plane waves $k=(k,0,0)$). Axis stencils are blind to the known anisotropy of the Freudenthal continuum moment tensor, so these lemmas support only that sector.
proof idea
One-line wrapper. After unfolding unitVec 2 = (0,0,1), the first component of the sum is the first component of $x$ plus zero, which is discharged by the integer add_zero identity (from the foundation arithmetic layer). Marked @[simp] so later stencil expansions can fire it automatically.
why it matters
Feeds two parent theorems in the same file. planeH_transverse uses it (with the e0 and e1 siblings) inside a simp only that shows the discrete divergence of an axis plane wave with vanishing first polarization row is identically zero. discLap3_planeH uses the same family of projection facts to prove that an axis plane wave is an eigenvector of the 3D discrete Laplacian with the same eigenvalue as the 1D mode, because the y- and z-stencils act trivially on a mode constant in those directions.
That 3D eigenvector identity is the lattice half of the axis-sector bridge from discrete perturbation spectrum to the continuum Lichnerowicz operator on the flat 3-torus. It does not close isotropic full-spectrum recovery; direction-resolved symbol questions remain under the C10 probe.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.