laplacian_continuum_limit
plain-language theorem explainer
The centered second difference of a C⁴ real function converges to its second derivative at rate O(a²). Anyone working the cubic-lattice Regge → continuum bridge cites this as the 1D finite-difference engine. The proof is a one-line wrapper that reuses the existing continuum second-order limit and drops the nonnegativity witness on the constant.
Claim. For $f:\mathbb{R}\to\mathbb{R}$ of class $C^4$, any $x\in\mathbb{R}$, and any mesh $a\neq 0$, there exists $C\in\mathbb{R}$ such that $\bigl|\frac{f(x+a)+f(x-a)-2f(x)}{a^2}-f''(x)\bigr|\le C\,a^2$.
background
The module replaces the general Cheeger–Müller–Schrader axiom by a direct cubic-lattice argument for J-cost interactions on $\mathbb{Z}^D$. Tier 3 of that strategy is lattice-to-continuum passage for the discrete Laplacian.
The object here is the standard centered second difference $(f(x+a)+f(x-a)-2f(x))/a^2$. Upstream, continuum_limit_second_order already proves that for $C^4$ data this equals $f''(x)$ plus an $O(a^2)$ remainder controlled by a fourth-derivative bound (explicitly $(a^2/12)f^{(4)}(\xi)$ in the Taylor form). Spatial dimension $D=3$ is forced elsewhere in the RS chain (T8), but this lemma is purely 1D analytic.
The next sibling note in the file records that the 3D lattice Laplacian is the sum of three independent 1D second-difference operators, so the 1D bound lifts coordinatewise.
proof idea
One-line term wrapper. Unpack the existential from continuum_limit_second_order (which returns a nonnegative $C$ and the error inequality), then re-pack just $C$ and the inequality, discarding the $0\le C$ conjunct. No new analysis is performed.
why it matters
This is Tier 3 of the cubic Regge convergence program in the module doc: lattice Laplacian$/a^2\to\nabla^2$ at $O(a^2)$. Combined with Tier 1 (J-cost action within $O(\varepsilon_{\max}^4)$ of the quadratic action) and Tier 2 (EL linearization via $\sinh'(0)=1$ to the lattice Laplacian), it closes the claim that the J-cost variational principle on $\mathbb{Z}^D$ converges to the continuum linearized Einstein equation at $O(a^2)$.
It therefore discharges the continuum half of the direct replacement for the CMS axiom in the RS-specific cubic setting, where the cost is the forced $J(\mathrm{e}^\varepsilon)=\cosh\varepsilon-1$ rather than a generic edge weight. No downstream consumers are wired yet in the graph; the intended landing is the full lattice-to-EFE convergence package for zero-parameter gravity.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.