continuum_limit_certificate
plain-language theorem explainer
Five continuum-limit ingredients are packaged as one certificate: the log-cost is quadratic to leading order with an O(ε⁴) bound, is even (CPT), vanishes at vacuum, and the lattice Laplacian kills constants and is linear. Anyone deriving continuum field equations from discrete J-cost dynamics cites this. The proof is a pure conjunction of five already-proved lemmas.
Claim. The following hold simultaneously: (i) for all real $\varepsilon$ with $|\varepsilon|<1$, $|J_{\log}(\varepsilon)-\varepsilon^2/2|\le|\varepsilon|^4/20$; (ii) $J_{\log}(-t)=J_{\log}(t)$ for all real $t$; (iii) $J_{\log}(0)=0$; (iv) on $\mathbb{Z}^D$, the lattice Laplacian of any constant field is identically zero; (v) the lattice Laplacian is additive in its field argument.
background
Module F-014 shows how discrete J-cost dynamics on the ledger lattice produce smooth continuum physics. RS is fundamentally discrete (ticks, voxels, ledger entries), yet observed physics is written in continuous PDEs. The bridge is the Taylor structure of the cost.
In log coordinates the cost is $J_{\log}(t)=\cosh t-1$, a convex bowl minimized at $t=0$. Its expansion $\cosh t-1=t^2/2+t^4/24+\cdots$ makes the leading small-perturbation cost quadratic. A lattice field on $\mathbb{Z}^D$ is a real-valued assignment of log-ratio perturbations to sites. The lattice Laplacian 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)$.
Upstream, $J_{\log}$ and its quadratic approximation, evenness, and zero-at-origin come from DiscretenessForcing; constancy and additivity of the lattice Laplacian are proved in this module. Spatial dimension $D=3$ is forced elsewhere (T8/T9), but the certificate itself is stated for general $D$.
proof idea
Term-mode packaging: the five conjuncts are discharged by naming five prior results. Quadratic remainder uses J_log_quadratic_approx; evenness uses J_log_symmetric; vacuum uses J_log_zero. Constancy and additivity of the lattice Laplacian are the already-proved lattice_laplacian_const and lattice_laplacian_add, each applied under a trivial binder for dimension, field, and site. No new algebra is performed here.
why it matters
This is the F-014 continuum-limit certificate: the discrete ledger is forced toward free scalar continuum physics rather than choosing it. The doc-comment chain is explicit: RCL uniquely fixes $J=\cosh-1$ (T5), the $t^2/2$ leading term yields the lattice Laplacian, continuum scaling yields $\nabla^2$, and with a mass from the $\phi$-ladder one obtains Klein-Gordon structure; higher Taylor terms seed interactions. CPT evenness of $J_{\log}$ is the discrete seed of continuum CPT.
Downstream, Gravity.ContinuumManifoldEmergence re-exports a continuum-limit certificate as part of manifold-emergence bookkeeping (signature and causal classification). The present theorem supplies the cost-and-Laplacian half of that story: quadratic leading order, vacuum, CPT, and linear lattice Laplacian with kernel on constants. It does not itself construct the scaling limit or the KG equation; those sit in sibling results of the same module (lattice_laplacian_limit, klein_gordon_structure, universality).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.