shift_minus
plain-language theorem explainer
Defines the unit backward lattice shift on ℤ^D: decrement the k-th integer coordinate of a site x by one. Anyone writing nearest-neighbor sums, lattice Laplacians, or discrete Euler–Lagrange operators on the recognition lattice cites it. The body is a one-line Function.update that replaces x_k by x_k − 1.
Claim. For dimension $D\in\mathbb{N}$, direction $k\in\{0,\ldots,D-1\}$, and lattice site $x:\{0,\ldots,D-1\}\to\mathbb{Z}$, the backward shift is the point $x-e_k$ obtained by decreasing the $k$-th coordinate by one and leaving all other coordinates fixed.
background
Module F-014 (ContinuumLimit) shows how discrete J-cost dynamics on the ledger lattice produce smooth continuum physics. The bridge is: small-perturbation J-cost is quadratic, quadratic nearest-neighbor cost is the lattice Laplacian, and that Laplacian scales to $\nabla^2$, yielding Klein–Gordon structure (and later Dirac/Einstein structure in $D=3$).
Sites are maps $x:\mathrm{Fin},D\to\mathbb{Z}$, i.e. points of $\mathbb{Z}^D$. A lattice field is a real-valued function on those sites. Nearest-neighbor calculus needs the two unit shifts along each axis: forward ($+e_k$) and backward ($-e_k$). Spatial dimension $D$ is the forced value $3$ from the T8/T9 chain elsewhere in the monolith, but the shift itself is written for general $D$.
This definition is the pure geometric primitive for the minus direction; its twin is the forward shift. Downstream objects (lattice Laplacian, neighbor J-cost, discrete EL operator) sum over both.
proof idea
Not a theorem: a definition. The implementation is Mathlib's Function.update: copy the coordinate tuple $x$ and overwrite coordinate $k$ with $x_k-1$. No lemmas are applied; the term is the entire meaning.
why it matters
Without a named backward shift, every nearest-neighbor formula in F-014 would inline coordinate surgery. The lattice Laplacian is $\sum_k\bigl(f(x+e_k)+f(x-e_k)-2f(x)\bigr)$; neighbor cost sums $J_{\log}$ on the same pairs; the discrete Euler–Lagrange operator uses $\sinh$ differences across the same edges. Those feed jcost_gives_laplacian_structure, Gravity's jcost_neighbor_is_laplacian, and the Cubic Regge convergence certificate (EL $\to$ Laplacian $\to\nabla^2$ tiers). In the RS chain this is the discrete geometry step that turns T5's J-cost and T8's $D=3$ into continuum $\nabla^2$ physics (registry F-014).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.