fst_sub_e1
plain-language theorem explainer
On the integer lattice ℤ³, shifting a site by the y-axis unit vector leaves the x-coordinate unchanged. Anyone simplifying the 3D axis-stencil Laplacian on plane waves constant in y and z will hit this identity. The proof is a one-line appeal to subtraction by 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_y$ equals $x_1$, where $e_y = (0,1,0)$ is the unit step along the second axis.
background
The module develops the discrete Lichnerowicz operator on the flat 3-torus as part of the Seven-Gaps Lane 4 (operator convergence) campaign. Lattice sites are represented as Site3 := ℤ × ℤ × ℤ, with the torus reading coming from N-periodicity along each axis rather than from ZMod arithmetic.
Axis unit steps are packaged as unitVec : Fin 3 → Site3, with unitVec 1 = (0,1,0). Component projections on product types are the standard .1, .2, .3. The surrounding development works exclusively in the axis-stencil sector: plane waves of the form $k = (k,0,0)$ acted on by the componentwise discrete Laplacian. Axis stencils are blind to the known anisotropy of the Freudenthal frozen energy, so these identities support only axis-sector spectral statements.
proof idea
One-line wrapper. Expanding the definition, $x - \mathrm{unitVec},1 = (x_1 - 0,, x_2 - 1,, x_3 - 0)$, so the first projection is $x_1 - 0$. The proof applies sub_zero to discharge that equality.
why it matters
Feeds directly into discLap3_planeH, the 3D eigenvector identity: an axis plane wave constant in $y$ and $z$ is an eigenvector of the 3D discrete Laplacian with the same eigenvalue as the corresponding 1D Fourier mode, because the $y$ and $z$ stencil shifts act trivially on such modes. This lemma is the coordinate bookkeeping that lets those $y$-shifts drop out of the first component when the stencil is expanded.
In the broader Recognition Gravity stack it is scaffolding for the discrete-to-continuum Lichnerowicz spectrum on the flat 3-torus (Lane 4). It does not itself touch the forcing chain T0–T8, the RCL, or the $\varphi$-ladder; it is pure lattice arithmetic supporting the axis-sector convergence tier flagged in the module doc.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.