shift_plus
plain-language theorem explainer
Unit positive lattice shift along a coordinate axis: given dimension D, axis k, and site x in Z^D, return x with the k-th coordinate increased by one. Every nearest-neighbor construction in the continuum-limit and cubic-Regge pipelines cites it (lattice Laplacian, neighbor J-cost, Euler-Lagrange). The body is a one-line Function.update.
Claim. For $D \in \mathbb{N}$, axis index $k \in \{0,\ldots,D-1\}$, and lattice site $x \in \mathbb{Z}^D$, the positive unit shift is $(x + e_k)_i = x_i + \delta_{ik}$: only the $k$-th coordinate increases by $1$.
background
Module F-014 (ContinuumLimit) shows how discrete J-cost dynamics on the integer lattice $\mathbb{Z}^D$ produce, in the long-wavelength limit, a second-order diffusion structure matching Klein-Gordon. The bridge is: J-cost $\to$ quadratic cost $\to$ lattice Laplacian $\to$ continuous $\nabla^2$.
Lattice sites are maps $x : \mathrm{Fin}, D \to \mathbb{Z}$. Nearest-neighbor geometry needs the two unit steps $\pm e_k$ along each axis. This definition supplies the positive step; its sibling shift_minus supplies the negative one. Spatial dimension $D$ is forced to $3$ by the T8/T9 chain (GapDerivation, AlphaDerivation), though the shift itself is written for general $D$.
A lattice field is a real-valued function on $\mathbb{Z}^D$. Differences $f(x+e_k)-f(x)$ feed both the neighbor J-cost and the discrete Laplacian that appear downstream.
proof idea
Pure definition, not a proof. The body is Function.update x k (x k + 1): copy the coordinate tuple and replace the $k$-th entry by $x_k+1$. No lemmas are invoked.
why it matters
This is the primitive positive edge of the cubic lattice used throughout F-014 and the gravity continuum pipeline. Downstream, lattice_laplacian sums $f(x+e_k)+f(x-e_k)-2f(x)$ over axes; neighbor_cost sums $J_{\log}$ of the same neighbor differences; jcost_gives_laplacian_structure proves that in the small-perturbation regime those costs reduce to the quadratic Laplacian form.
Gravity reuses it: jcost_neighbor_is_laplacian (ContinuumManifoldEmergence), and in CubicReggeProof the Euler-Lagrange operator, the 3D Laplacian decomposition, and the linearized EL $= -\Delta$ identity all evaluate fields at shift_plus k x. The CubicReggeConvergenceCert package that replaces the old Regge-to-EH axioms therefore depends on this shift as lattice infrastructure.
Framework role: it is the discrete geometry step that lets J-cost dynamics on $\mathbb{Z}^3$ (T8: $D=3$) become $\nabla^2$ and thence Klein-Gordon structure in the continuum limit (registry F-014).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.