emergence_error
plain-language theorem explainer
Explicit residual-error bound for each continuum-emergence stage as a function of the perturbation size ε. Quadratic and continuum stages share the fourth-order remainder |ε|⁴/20; the interacting stage tightens to sixth order |ε|⁶/720. The hierarchy theorem cites it to order these accuracies for |ε|<1. Pure case-split definition from Taylor remainders of the J-cost.
Claim. For each continuum-emergence stage $\ell$ and real perturbation $\varepsilon$, the residual approximation error is $|\varepsilon|^4/20$ when $\ell$ is the quadratic or continuum stage, and $|\varepsilon|^6/720$ when $\ell$ is the interacting stage.
background
Module F-014 shows how discrete J-cost dynamics on the lattice $\mathbb{Z}^3$ produce smooth continuum physics. The cost $J(e^t)=\cosh(t)-1$ expands as $t^2/2+t^4/24+\cdots$. For small perturbations $t=\varepsilon\delta$ with $\varepsilon\to 0$, the leading quadratic term yields a lattice Laplacian, which scales to continuous $\nabla^2$ and thence to Klein-Gordon structure (with mass from the $\varphi$-ladder).
EmergenceLevel packages the three stages of that limit: (1) quadratic regime, where $J(e^t)\approx t^2/2$ gives diffusion on the lattice; (2) continuum limit, lattice Laplacian $\to\nabla^2$ and free Klein-Gordon; (3) interacting regime, higher-order corrections. Each stage is characterized by the accuracy of its approximation, which this definition records as an explicit real-valued residual in $\varepsilon$.
proof idea
Definition by exhaustive match on the three constructors of EmergenceLevel. Quadratic and continuum both return $|\varepsilon|^4/20$ (fourth-order Taylor remainder of $\cosh$). Interacting returns $|\varepsilon|^6/720$ (sixth-order remainder). No lemmas are invoked; the body is a pure case assignment of remainder constants.
why it matters
Supplies the quantitative error measure that emergence_hierarchy compares: for $|\varepsilon|<1$, the interacting residual is at most the quadratic residual. That hierarchy is the accuracy ladder inside F-014's continuum-emergence story (J-cost $\to$ lattice Laplacian $\to\nabla^2\to$ Klein-Gordon). It makes precise the claim that each stage improves the approximation for small perturbations, closing the discrete-to-smooth gap that RS must fill before matching observed continuum field equations. Downstream only the hierarchy theorem consumes it directly; the constants themselves encode the Taylor structure of $J$ forced earlier in the chain (T5 J-uniqueness).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.