axis_second_diff
plain-language theorem explainer
The axis second difference is the discrete second derivative of a lattice field along one coordinate direction: f(x+e_k)+f(x-e_k)-2f(x). Continuum-limit and lattice-gravity arguments cite it as the atomic 1D stencil inside the multi-dimensional lattice Laplacian. The definition is the standard three-point central difference on the product lattice Z^D.
Claim. For a lattice field $f:\mathbb{Z}^D\to\mathbb{R}$ and axis index $k\in\{0,\ldots,D-1\}$, the second difference of $f$ along axis $k$ at site $x$ is $f(x+e_k)+f(x-e_k)-2f(x)$, where $e_k$ is the unit lattice shift along coordinate $k$.
background
This module lifts the 1D continuum-limit second-order result to the full product lattice $\mathbb{Z}^D$, with $D=3$ forced by the Recognition forcing chain (T8). A lattice field is a real-valued map on sites $x\in\mathbb{Z}^D$; each site carries a log-ratio perturbation. Single-axis shifts move $x$ by $\pm 1$ along coordinate $k$ only.
The D-dimensional lattice Laplacian is defined as the sum over axes of the three-point stencil $f(x+e_k)+f(x-e_k)-2f(x)$. That stencil is exactly the object named here. In the continuum limit (spacing $a\to 0$) each such term becomes $a^2\partial_k^2 f+O(a^4)$, so the sum becomes $a^2\nabla^2 f$ plus higher-order error.
Gravity connection: the lattice Laplacian is the kinetic operator in the lattice action; after continuum limit it supplies $\nabla^2$ on metric perturbations, hence the linearized Ricci piece $R_{\mu\nu}\sim\nabla^2 h_{\mu\nu}$ in harmonic gauge.
proof idea
Pure definition: the body is the three-term central difference $f(\mathrm{shift}+^k x)+f(\mathrm{shift}-^k x)-2f(x)$, using the single-axis lattice shifts from ContinuumLimit. No proof obligations; noncomputable only because the ambient real-valued field type is.
why it matters
This is the atomic 1D building block for the module's main decomposition theorem: the lattice Laplacian equals the sum over $k$ of these axis second differences. That identity feeds the certificate structure LatticeConvergenceCert (three_terms and decomposition fields) and the D=3 convergence theorem that the scaled lattice Laplacian tends to $\nabla^2$ with $O(a^2)$ error.
In the Recognition framework this closes Step 1 of multi-dimensional lattice Laplacian convergence, extending the 1D continuum_limit_second_order result to the forced spatial dimension $D=3$. Downstream J-cost neighbor approximations on $\mathbb{Z}^3$ rely on the same stencil sum, linking discrete recognition cost to continuum gravity kinetics.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.