emergence_hierarchy
plain-language theorem explainer
For every real perturbation with absolute value strictly less than one, the continuum-emergence error at the interacting truncation is at most the error at the pure quadratic truncation. Anyone tracking how successive Taylor cuts of J refine the lattice-to-continuum map would cite this. The proof unfolds the error functional, bounds powers of |ε| under |ε|<1, and closes by nonlinear arithmetic.
Claim. Let $\varepsilon\in\mathbb{R}$ satisfy $|\varepsilon|<1$. Then the emergence error of the interacting approximation at scale $\varepsilon$ is at most the emergence error of the quadratic approximation at the same scale: $E_{\mathrm{int}}(\varepsilon)\le E_{\mathrm{quad}}(\varepsilon)$.
background
Module F-014 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 cost is $J(e^t)=\cosh(t)-1$, with Taylor series $t^2/2+t^4/24+\cdots$. For small perturbations $t=\varepsilon\delta$ with $\varepsilon\to 0$, the leading $t^2/2$ term is a quadratic cost; quadratic costs on a lattice yield the discrete Laplacian, which scales to continuous $\nabla^2$.
The second derivative normalization $J''(1)=1$ (from Cost.Convexity) fixes the quadratic coefficient and the mass scale. Successive truncations of the cosh series define approximation levels: quadratic (keep $t^2/2$), then interacting (include higher even powers fixed by cosh). The quantity emergence_error measures the remainder of each truncation at a given $\varepsilon$.
The local claim is the hierarchy among those remainders for $|\varepsilon|<1$: refining the truncation cannot increase the error bound in that disk.
proof idea
Tactic proof. Unfold the emergence-error definition at both levels, exposing explicit polynomial expressions in $|\varepsilon|$. From $|\varepsilon|<1$ and nonnegativity of absolute value, obtain $|\varepsilon|^2\le 1$ and $|\varepsilon|^4\le 1$ by pow_le_one₀. Positivity gives $|\varepsilon|^4\ge 0$. A short calc then shows $|\varepsilon|^6=|\varepsilon|^4\cdot|\varepsilon|^2\le|\varepsilon|^4$. With those power comparisons in hand, nlinarith discharges the desired inequality between the two unfolded error expressions. No external named lemmas beyond elementary absolute-value and power facts are required.
why it matters
This sits in the continuum-limit chain of F-014: J-cost on $\mathbb{Z}^3$ $\to$ lattice Laplacian $\to$ continuous $\nabla^2$ $\to$ Klein-Gordon structure, with mass from the $\phi$-ladder. The hierarchy justifies reading the interacting truncation as a refinement of the Gaussian (quadratic) universality class rather than a competing continuum limit.
It supports the module's claim that J selects the universality class: even symmetry of $\cosh(t)-1$ gives $t\mapsto -t$ (equivalently $x\mapsto 1/x$) invariance and CPT; Taylor coefficients $1/2,1/24,1/720,\ldots$ are fixed by cosh with no free couplings; the quadratic coefficient matches $J''(1)=1$. RCL uniqueness of $J$ (forcing chain T5) therefore uniquely forces this continuum hierarchy.
No downstream consumers are recorded yet (used_by empty). The result is a proved local comparison inside the continuum-limit development, not a top-level forcing step (T0–T8).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.