unitVec
plain-language theorem explainer
Standard lattice basis on the flat 3-torus: index a in {0,1,2} maps to the integer displacement e_a along that axis. Anyone writing discrete divergence or Laplacian stencils on Site3 cites it. The body is a three-clause pattern match, not a proof.
Claim. Define the lattice unit vectors $e_a$ for $a \in \{0,1,2\}$ by $e_0 = (1,0,0)$, $e_1 = (0,1,0)$, $e_2 = (0,0,1)$ as elements of $\mathbb{Z}^3$ (the 3D lattice site type for the flat 3-torus).
background
This module develops the discrete Lichnerowicz operator on the flat 3-torus as part of the Seven-Gaps campaign (Lane 4: operator convergence). Lattice sites are Site3, an abbreviation for $\mathbb{Z} \times \mathbb{Z} \times \mathbb{Z}$, read periodically as the flat torus; fields are $N$-periodic functions rather than data on ZMod N, so stencil identities hold pointwise on $\mathbb{Z}$.
Axis unit steps are the elementary displacements used by every forward-difference and second-difference stencil. The file restricts convergence claims to the axis-stencil sector (plane waves $k=(k,0,0)$ under the componentwise axis Laplacian), so these three vectors are exactly the directions the discrete operators probe.
Upstream, only the site type is needed: once sites are integer triples, the unit vectors are the canonical generators of nearest-neighbor shifts along each coordinate.
proof idea
No proof: a definition by cases on Fin 3. Index 0 returns $(1,0,0)$, index 1 returns $(0,1,0)$, index 2 returns $(0,0,1)$. Downstream simp lemmas such as fst_add_e0 and fst_sub_e0 then reduce coordinate arithmetic by rfl or add_zero.
why it matters
This is the shared geometric primitive for the discrete calculus in the file. The discrete divergence discDiv sums forward differences $H(x+e_a)-H(x)$ over $a$, and the 3D Laplacian discLap3 sums the three 1D second-difference stencils at $\pm e_a$, both scaled by powers of $N$. The coordinate lemmas fst_add_e* / fst_sub_e* exist only to make those shifts compute under simplification.
In the broader Recognition gravity program this supports the first Lean bridge from lattice perturbation spectra to the continuum Lichnerowicz operator on a flat $T^3$ background (not the vacuous older GW files). It does not itself close the isotropic symbol question: axis stencils are blind to the anisotropic Freudenthal moment tensor flagged in the module scope, so full flat-space Lichnerowicz recovery remains a separate C10/P-iso item. Framework-wise it sits under the $D=3$ spatial setting (T8) as lattice infrastructure, not a forcing-chain step.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.