relative_error_vanishes
plain-language theorem explainer
The relative error between the log-coordinate J-cost and its quadratic leading term vanishes as the perturbation goes to zero: for nonzero ε with |ε|<1, |J_log(ε)−ε²/2|/(ε²/2) ≤ ε²/10. Anyone arguing that discrete J-dynamics produce continuum Laplacian (then Klein–Gordon) physics cites this bound. The proof is a short algebraic rearrangement of the absolute O(ε⁴) estimate already proved upstream.
Claim. Let $J_{\log}(\varepsilon)=\cosh(\varepsilon)-1$ and write the quadratic leading cost as $\varepsilon^2/2$. For every real $\varepsilon$ with $0<|\varepsilon|<1$, $$\frac{|J_{\log}(\varepsilon)-\varepsilon^2/2|}{\varepsilon^2/2}\le\frac{\varepsilon^2}{10}.$$ Thus the relative error of the quadratic approximation tends to $0$ as $\varepsilon\to 0$.
background
Module F-014 (ContinuumLimit) 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 Taylor expansion of the cost in log coordinates: $J(e^t)=\cosh(t)-1=t^2/2+t^4/24+\cdots$. Small perturbations therefore look quadratic, and quadratic lattice costs generate discrete Laplacians that continuum-limit to $\nabla^2$.
Here $J_{\log}(t):=\cosh(t)-1$ is the convex bowl centered at the identity (from DiscretenessForcing). The sibling definition quadratic_cost is exactly the leading term $\varepsilon^2/2$. Upstream, jcost_quadratic_leading already supplies the absolute error bound $|J_{\log}(\varepsilon)-\varepsilon^2/2|\le|\varepsilon|^4/20$ whenever $|\varepsilon|<1$, itself a thin wrapper of the Taylor remainder for cosh.
The present statement upgrades that absolute $O(\varepsilon^4)$ control to a relative-error statement normalized by the quadratic cost itself, which is the form needed when one later compares neighbor costs and extracts a lattice Laplacian.
proof idea
One short tactic proof. First invoke jcost_quadratic_leading to obtain $|J_{\log}\varepsilon-\varepsilon^2/2|\le|\varepsilon|^4/20$. Positivity of quadratic_cost ($\varepsilon^2/2>0$ for $\varepsilon\ne 0$) lets one clear the denominator via div_le_div_iff₀, turning the goal into an inequality between absolute error and $(\varepsilon^2/2)\cdot(\varepsilon^2/10)$. After rewriting $|\varepsilon|^4=\varepsilon^4$ (via sq_abs), nlinarith finishes with the nonnegativity facts sq_nonneg ε and sq_abs ε. No new analytic input beyond the upstream absolute bound.
why it matters
This is the quantitative “quadratic becomes exact” step in the F-014 continuum program. The module narrative is: J-cost on $\mathbb{Z}^3$ → quadratic leading term → lattice Laplacian → continuous $\nabla^2$ → Klein–Gordon (mass from the $\varphi$-ladder) → Dirac (spinor structure in $D=3$) → Einstein (defect curvature). Without a vanishing relative error, the identification of the discrete cost with a pure Laplacian would retain uncontrolled higher-order pollution at every scale.
It sits immediately after jcost_quadratic_leading and quadratic_cost in the same file, and is the natural hypothesis for the later lattice-field and neighbor-cost constructions (LatticeField, lattice_laplacian, neighbor_cost). No downstream theorem yet records a direct used_by edge, so the lemma is presently a proved leaf waiting on the Laplacian-limit and Klein–Gordon-structure results listed in the module doc. Framework landmarks touched: T5 J-uniqueness (the cost being approximated), T8 $D=3$, and the eight-tick discrete ledger whose long-wavelength limit this module justifies.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.