jcost_gives_laplacian_structure
plain-language theorem explainer
Under small nearest-neighbor field jumps (|Δf|<1 on every axis), the J-cost summed over ± neighbors equals the discrete Dirichlet energy (half sum of squared jumps) up to an explicit O(|Δf|⁴) remainder. Continuum and gravity authors cite it as the bridge from ledger cost to lattice Laplacian. The proof applies the quadratic leading expansion per bond, then triangle inequality and sum bounds.
Claim. Let $f:\mathbb{Z}^D\to\mathbb{R}$ be a lattice field and $x\in\mathbb{Z}^D$. If for every axis $k$ one has $|f(x+e_k)-f(x)|<1$ and $|f(x-e_k)-f(x)|<1$, then $$\Bigl|\mathrm{neighbor\_cost}(f,x)-\sum_{k=1}^{D}\tfrac12\bigl((f(x+e_k)-f(x))^2+(f(x-e_k)-f(x))^2\bigr)\Bigr|\le\sum_{k=1}^{D}\Bigl(\frac{|f(x+e_k)-f(x)|^4}{20}+\frac{|f(x-e_k)-f(x)|^4}{20}\Bigr).$$
background
Module F-014 (Continuum Limit) shows how discrete J-cost dynamics on $\mathbb{Z}^D$ produce smooth second-order PDEs. The cost is $J_{\log}(\varepsilon)=\cosh(\varepsilon)-1$ (equivalently the T5 unique $J$), with Taylor expansion $\varepsilon^2/2+\varepsilon^4/24+\cdots$. In the long-wavelength regime the quadratic piece dominates and lattice quadratic energies yield discrete Laplacians, which scale to $\nabla^2$ and thence Klein–Gordon structure.
A lattice field is a map $f:(\mathrm{Fin},D\to\mathbb{Z})\to\mathbb{R}$ assigning a log-ratio perturbation to each site. Shifts $x\pm e_k$ move one step along axis $k$. Neighbor cost sums $J_{\log}$ of the forward and backward jumps at $x$. Upstream, jcost_quadratic_leading states: if $|\varepsilon|<1$ then $|J_{\log}\varepsilon-\varepsilon^2/2|\le|\varepsilon|^4/20$, the per-bond bridge from discrete cost to quadratic energy.
proof idea
Unfold neighbor cost into a sum over axes of $J_{\log}$ on $\pm$ jumps. For each axis $k$, the smallness hypothesis supplies $|\Delta_\pm f|<1$, so jcost_quadratic_leading bounds each bond error by $|\Delta_\pm f|^4/20$. Write the two-bond discrepancy as $A+B$ (plus-minus residual after subtracting $\varepsilon^2/2$); triangle inequality and linarith give the per-axis bound.
Lift to the full sum: rewrite the absolute difference of sums as the absolute value of the sum of per-axis residuals (Finset.sum_sub_distrib), apply Finset.abs_sum_le_sum_abs, then Finset.sum_le_sum with the per-axis bound. No continuum scaling is used here; only finite-dimensional real arithmetic and the quadratic leading lemma.
why it matters
This is the lattice-level statement that variational J-cost dynamics produce diffusion: the gradient of the quadratic neighbor energy is (minus) the lattice Laplacian, so minimizing J yields Laplacian flow. Downstream, Gravity.ContinuumManifoldEmergence specializes it at $D=3$ as jcost_neighbor_is_laplacian. CubicReggeProof wires it into proved_convergence_chain as step2_neighbor_approx and into total_action_convergence (total J-cost approximates quadratic action with $\sum|\varepsilon|^4/20$ error). LatticeConvergence uses it for the 3D neighbor approximation and second-order convergence claims.
In the RS chain it sits after T5 J-uniqueness and the continuum module’s quadratic expansion, and before continuum $\nabla^2$, Klein–Gordon (mass from the $\phi$-ladder), and the Regge/EFE convergence story. It closes the discrete-to-Laplacian half of registry item F-014 without axioms or sorry.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.