GaussianUniversality
plain-language theorem explainer
Packages Gaussian universality for the Recognition Science log-cost: near equilibrium the cost is quadratic with a controlled quartic remainder. Continuum and free-field derivations cite this interface when passing from discrete ledger dynamics to a Klein-Gordon continuum. Both fields state the same small-ε bound, so an instance is just a witness of that Taylor control; no separate RG argument lives in the structure.
Claim. A record of Gaussian universality for the log-coordinate cost $J_{\log}(\varepsilon)=\cosh\varepsilon-1$. It requires that for every real $\varepsilon$ with $|\varepsilon|<1$, $$|J_{\log}(\varepsilon)-\varepsilon^2/2|\le|\varepsilon|^4/20.$$ The same inequality is stored twice: once as the leading quadratic approximation and once as quartic remainder control (higher orders are treated as irrelevant under renormalization-group flow).
background
Module F-014 (Continuum Limit) explains how discrete J-cost dynamics on the lattice $\mathbb{Z}^3$ produce smooth physics. The cost in log coordinates is $J_{\log}(t)=\cosh t-1$, a convex bowl minimized at $t=0$. Its Taylor series is $t^2/2+t^4/24+\cdots$. In the long-wavelength regime (small perturbations), the quadratic piece dominates and induces a lattice Laplacian, which scales to the continuum $\nabla^2$ and thence to Klein-Gordon structure.
Upstream, $J_{\log}$ is the standard log-coordinate form of the unique J-cost forced by the Recognition Composition Law (T5): $J(e^t)=\cosh t-1$. Sibling results such as the quadratic leading expansion and relative-error vanishing make the $O(\varepsilon^4)$ remainder precise. Cost notions elsewhere in the stack (observer events, multiplicative recognizers, rung coarsening) all reduce to this same J-shape, so the continuum analysis is not tied to one encoding.
proof idea
This declaration is a structure (a Prop-valued interface), not a proved theorem. It names two fields that currently carry identical statements: for $|\varepsilon|<1$, the absolute deviation of $J_{\log}\varepsilon$ from $\varepsilon^2/2$ is at most $|\varepsilon|^4/20$. There is no proof body; discharge happens at instance construction. Downstream, the witness theorem fills both fields by the same quadratic-approximation lemma for $J_{\log}$, so the structure is a thin packaging of that Taylor bound under the Gaussian-universality label from the module plan.
why it matters
F-014's main list ends with universality class membership: the J-cost system sits in the Gaussian class, so the continuum limit is free-field (Klein-Gordon), with interactions only from higher-order ($t^4$) corrections. This structure is the typed carrier of that claim; the sole direct consumer builds an instance asserting that the RS J-cost system satisfies Gaussian universality, then the module moves on to Klein-Gordon structure.
In the broader forcing chain, T5 fixes $J(x)=(x+x^{-1})/2-1$ (equivalently $\cosh(\log x)-1$), and the continuum bridge turns that unique cost into lattice then continuum Laplacians on $\mathbb{Z}^3$ (T8). Gaussian universality is the renormalization-group reading of the same expansion: quadratic fixed point stable in the infrared, quartic terms irrelevant. It does not by itself produce masses or couplings; those enter later via the $\phi$-ladder and higher-order remainders.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.