quadratic_approximates_jlog
plain-language theorem explainer
For |ε| < 1, the log-coordinate J-cost differs from the pure quadratic ε²/2 by at most |ε|⁴/20. Continuum-limit and lattice-field arguments cite this O(ε⁴) match when replacing discrete J-dynamics by a quadratic cost. The proof is a one-line unfold of the quadratic cost definition followed by the leading Taylor remainder for cosh.
Claim. For every real $\varepsilon$ with $|\varepsilon| < 1$, $\bigl|(\cosh\varepsilon - 1) - \varepsilon^2/2\bigr| \le |\varepsilon|^4/20$.
background
Module F-014 (Continuum Limit) shows how discrete J-cost dynamics on the lattice $\mathbb{Z}^3$ produce, in the long-wavelength limit, a second-order diffusion structure matching Klein-Gordon. The bridge is the small-perturbation expansion of the cost.
In log coordinates the cost is $J_{\log}(t) = \cosh t - 1$, a convex bowl minimized at $t = 0$. Its Taylor series is $t^2/2 + t^4/24 + \cdots$. The leading piece is packaged as the quadratic cost $\varepsilon^2/2$. Upstream, jcost_quadratic_leading records the concrete remainder: for $|\varepsilon| < 1$, $|J_{\log}\varepsilon - \varepsilon^2/2| \le |\varepsilon|^4/20$, obtained from the standard cosh approximation lemma in DiscretenessForcing.
Quadratic costs on a lattice generate the discrete Laplacian; the continuum scaling limit of that Laplacian is $\nabla^2$. Hence the $O(\varepsilon^4)$ match is the first quantitative step from ledger ticks to smooth field equations.
proof idea
One-line wrapper. Unfold the definition of the quadratic cost (which is exactly $\varepsilon^2/2$), then apply the already-proved leading-order bound jcost_quadratic_leading at the same $\varepsilon$ and hypothesis $|\varepsilon| < 1$. No extra algebra is performed here; the numerical constant $1/20$ and the domain restriction are inherited verbatim from that upstream remainder estimate.
why it matters
This is the named interface between the exact J-cost and the quadratic surrogate used throughout the continuum program (registry F-014). The module arc is: J-cost $\to$ quadratic leading term $\to$ lattice Laplacian $\to$ continuous $\nabla^2$ $\to$ Klein-Gordon structure, with mass from the $\varphi$-ladder and $D = 3$ from the forcing chain (T8). The same expansion underlies the claim that the system sits in the Gaussian universality class.
Sibling results (relative_error_vanishes, neighbor and lattice-Laplacian lemmas) build on this $O(\varepsilon^4)$ control to show the relative error vanishes as $\varepsilon \to 0$ and that quadratic neighbor costs reproduce the discrete Laplacian. Even with no recorded downstream edges yet, the declaration is the citation point for any argument that replaces $J_{\log}$ by $\varepsilon^2/2$ inside a long-wavelength expansion. It sits downstream of T5 J-uniqueness ($J(x) = (x+x^{-1})/2 - 1 = \cosh(\log x) - 1$) via the log-coordinate form.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.