EmergenceLevel
plain-language theorem explainer
Three-stage taxonomy for how discrete J-cost dynamics on the lattice yield continuum field theory: quadratic (small-t diffusion), continuum (lattice Laplacian to ∇²), and interacting (t⁴ and higher corrections). Cited by anyone tracking approximation accuracy in the F-014 continuum-limit program. Pure inductive definition; no proof body.
Claim. An emergence level is one of three labels: quadratic (leading $J(e^{t})\approx t^{2}/2$), continuum (discrete Laplacian $\to$ continuous $\nabla^{2}$), or interacting ($t^{4}/24$ and higher corrections sourcing self-interactions).
background
Module F-014 asks how RS discrete ledger dynamics on $\mathbb{Z}^{3}$ produce the smooth PDEs of observed physics. The cost is $J(e^{t})=\cosh(t)-1$, with Taylor series $t^{2}/2+t^{4}/24+\cdots$. For long-wavelength perturbations $t=\varepsilon\delta$ with $\varepsilon\to 0$, the quadratic piece forces a lattice Laplacian; the continuum scaling limit of that Laplacian is $\nabla^{2}$, giving free Klein-Gordon structure (masses from the $\phi$-ladder). Higher even powers supply local interactions.
The three constructors name those successive regimes. Downstream, each level is paired with an explicit remainder bound so that error bookkeeping stays uniform across the chain from discrete J-dynamics to continuum PDEs.
proof idea
No proof: this is an inductive type with three nullary constructors. It is a pure classification tag used by matching definitions (notably the level-dependent error function).
why it matters
Gives the F-014 continuum program a single named stratification: quadratic regime $\to$ continuum limit $\to$ interacting theory, matching the module narrative from $J$-cost on $\mathbb{Z}^{3}$ through lattice Laplacian to $\nabla^{2}$, Klein-Gordon, and eventually $\phi^{4}$/SM-like corrections via the $\phi$-ladder. The sole recorded consumer is the level-indexed error map, which assigns $|\varepsilon|^{4}/20$ in the first two stages and $|\varepsilon|^{6}/720$ in the interacting stage. That keeps approximation claims auditable when later theorems assert Gaussian universality or Klein-Gordon form. Landmark link: T5 $J$-uniqueness supplies the cost whose expansion drives the stages; D=3 enters via the spatial lattice on which the Laplacian lives.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.