lattice_convergence_cert
plain-language theorem explainer
Packages three D=3 lattice-Laplacian facts into one certificate: the operator expands as three axis second-differences, equals the sum of independent 1D second-differences, and the scaled second difference converges to the continuum second derivative with O(a²) error. Continuum-limit and lattice-gravity arguments cite it as the assembled D=3 package. Proof is a term-mode structure instance wiring three already-proved lemmas.
Claim. There is a D=3 lattice-convergence certificate asserting: (i) for every lattice field $f$ on $\mathbb{Z}^3$ and site $x$, the lattice Laplacian equals the sum of the three axis second-differences $(f(x\pm e_i)-2f(x))$ for $i=0,1,2$; (ii) equivalently, it equals $\sum_{k\in\{0,1,2\}}$ of the one-dimensional axis second-difference along $k$; (iii) for every $a\neq 0$, every $C^4$ map $f:\mathbb{R}\to\mathbb{R}$, and every $x$, the scaled second difference $(f(x+a)+f(x-a)-2f(x))/a^2$ approximates $f''(x)$ up to an $O(a^2)$ remainder.
background
This module lifts the one-dimensional continuum-limit second-order result from ContinuumLimit to the product lattice $\mathbb{Z}^3$. The structural fact is that the D-dimensional lattice Laplacian is the sum of D independent one-dimensional second-difference operators, one per axis. Spatial dimension is fixed at three, matching the RS forcing step that selects $D=3$.
A lattice field on $\mathbb{Z}^3$ is a real-valued map on integer triples. The lattice Laplacian at a site is the sum, over the three coordinate directions, of neighbor values minus twice the on-site value. Each axis second-difference is the corresponding one-dimensional stencil. Scaling by $1/a^2$ and sending the lattice spacing $a\to 0$ is the continuum limit of the kinetic operator in a lattice action.
The certificate structure bundles three properties: the explicit three-term expansion, the sum-of-1D decomposition (for general D, specialized here), and the O(a²) convergence bound for the scaled second difference of a C⁴ test function. Upstream, the three-term identity is a Fin-sum simplification; the decomposition is definitional unfolding; convergence reuses the 1D second-order continuum limit along each axis.
proof idea
Term-mode structure instance: each field of the certificate is filled by an existing theorem. The three-term field is the D=3 expansion (unfold Laplacian, simplify the Fin-3 sum, ring). The decomposition field is the general identity that the lattice Laplacian equals the sum of axis second-differences (definitional). The convergence field is the D=3-labelled convergence theorem, which supplies the 1D O(a²) bound for ContDiff-4 test functions (each axis contributes an independent 1D error; the total remains O(a²)). No new calculation occurs at this declaration.
why it matters
In the gravity track, the lattice Laplacian is the kinetic operator of the lattice action. Its continuum limit is $\nabla^2$, which for metric perturbations in harmonic gauge yields the linearized Ricci contribution $R_{\mu\nu}\sim\nabla^2 h_{\mu\nu}$. Assembling the three-term count, the axis decomposition, and the O(a²) rate into one certificate marks Step 1 of multi-dimensional lattice convergence as closed for D=3.
The three-term count is the lattice shadow of the RS forcing result that spatial dimension is three (T8). The decomposition justifies reducing multi-D estimates to the 1D continuum-limit lemma already proved in ContinuumLimit. No downstream consumers are wired yet; the natural next use is feeding continuum-limit arguments for the lattice gravitational action and the J-cost neighbor approximation on $\mathbb{Z}^3$.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.