LatticeConvergenceCert
plain-language theorem explainer
A certificate packing three facts needed for continuum gravity on the cubic lattice: the Z^3 Laplacian expands as three nearest-neighbor second differences, equals the sum of independent axial second differences, and each scaled 1D second difference converges to the second derivative at O(a^2) for C^4 test functions. Gravity and continuum-limit arguments cite it as the typed bundle of those claims. Instantiation is by plugging in the three named lemmas; the structure itself carries no proof.
Claim. A certificate of lattice-to-continuum convergence in three spatial dimensions consists of: (i) for every field $f$ on $\mathbb{Z}^3$ and site $x$, the lattice Laplacian equals the sum of the three axial second differences $f(x\pm e_k)-2f(x)$; (ii) equivalently, $\Delta_{\mathrm{lat}} f(x)=\sum_{k=0}^{2}(\delta_k^2 f)(x)$; (iii) for every mesh $a\neq 0$, every $C^4$ function $f:\mathbb{R}\to\mathbb{R}$, and every $x\in\mathbb{R}$, there exists $C$ such that $\bigl|(f(x+a)+f(x-a)-2f(x))/a^2-f''(x)\bigr|\le C a^2$.
background
The module extends the one-dimensional continuum limit of second differences to the product lattice $\mathbb{Z}^3$. The lattice Laplacian in $D$ dimensions is the standard nearest-neighbor operator $$(\Delta_{\mathrm{lat}} f)(x)=\sum_k\bigl(f(x+e_k)+f(x-e_k)-2f(x)\bigr),$$ built from single-axis shifts that update only coordinate $k$ by $\pm 1$. On a product lattice the $D$-dimensional operator is exactly the sum of $D$ independent one-dimensional second-difference operators (one per axis).
LatticeField3 is the abbreviation for real-valued fields on $\mathbb{Z}^3$. The axial second difference along axis $k$ is the single term $f(x+e_k)+f(x-e_k)-2f(x)$. The continuum claim is the classical $O(a^2)$ consistency of the central second difference for $C^4$ functions, lifted coordinatewise.
In the gravity reading, this Laplacian is the kinetic operator of the lattice action; its continuum limit is $\nabla^2$, which for metric perturbations in harmonic gauge supplies the linearized Ricci piece $R_{\mu\nu}\sim\nabla^2 h_{\mu\nu}$.
proof idea
No proof body: the declaration is a structure whose three fields are propositions. A witness is assembled by assigning already-proved lemmas to those fields. Downstream, lattice_convergence_cert does exactly that: three_terms gets D3_laplacian_three_terms, decomposition gets lattice_laplacian_is_sum_of_1D, and convergence gets lattice_laplacian_3D_convergence. The structure only packages the interface.
why it matters
This certificate is the typed hand-off from the multi-dimensional lattice analysis to any gravity or continuum argument that needs a single object asserting "D=3 Laplacian = sum of three 1D pieces, and each piece converges at second order." Its sole consumer is lattice_convergence_cert, which fills the three slots and closes the Step-1 bundle of the module.
Framework-wise it specializes the continuum-limit story to the forced spatial dimension $D=3$ (forcing chain T8) and underwrites the kinetic term that becomes $\nabla^2$ in the continuum gravity action. It sits next to the J-cost neighbor approximation on $\mathbb{Z}^3$, which shows the Recognition cost expands to the same lattice Laplacian at $O(\varepsilon^4)$. Without this bundle, later linearized-curvature or continuum-action statements would re-prove the three facts ad hoc.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.