quadratic_cost
plain-language theorem explainer
Defines the leading-order continuum cost as ε²/2, the quadratic term in the Taylor expansion of J_log(ε) = cosh(ε) − 1. Continuum-limit and lattice-to-PDE arguments cite it as the Gaussian cost that yields the discrete Laplacian. The body is a one-line abbreviation, not a derived theorem.
Claim. The quadratic cost of a small log-coordinate perturbation $\varepsilon \in \mathbb{R}$ is $\varepsilon^2/2$.
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 starts from the log-coordinate cost $J_{\log}(t) = \cosh(t) - 1$, a convex bowl minimized at $t = 0$ (from DiscretenessForcing and the ContinuumBridge).
Its Taylor series is $\cosh(t) - 1 = t^2/2 + t^4/24 + \cdots$. For small perturbations $t = \varepsilon$ with $\varepsilon \to 0$, the leading term is quadratic. Quadratic costs on a lattice generate the discrete Laplacian, which scales to the continuous $\nabla^2$.
Related cost notions (ObserverForcing, MultiplicativeRecognizer, RungCoarsen, PRC bridge) all ultimately feed the same J-cost; this definition isolates the continuum leading piece used by the approximation lemmas in this module.
proof idea
Pure definition: quadratic_cost ε is bound to ε ^ 2 / 2. No tactics, no lemmas. Downstream theorems unfold it and apply jcost_quadratic_leading to compare against $J_{\log}$.
why it matters
This is the named leading term in the continuum emergence chain of F-014: J-cost on $\mathbb{Z}^3$ → quadratic cost → lattice Laplacian → continuous $\nabla^2$ → Klein–Gordon (mass from the $\varphi$-ladder) and onward. It is the cost that places the system in the Gaussian universality class.
Parents in-module: quadratic_approximates_jlog proves $|J_{\log}\varepsilon - \varepsilon^2/2| \le |\varepsilon|^4/20$ for $|\varepsilon| < 1$, and relative_error_vanishes shows the relative error is $O(\varepsilon^2)$ and vanishes as $\varepsilon \to 0$. Both unfold this definition. Ties to T5 J-uniqueness ($J(x) = (x+x^{-1})/2 - 1 = \cosh(\log x) - 1$) and the discrete-to-smooth gap the registry item F-014 addresses.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.