quartic_error_controlled
plain-language theorem explainer
For every real ε_max in (0,1), the quartic remainder ε_max⁴/24 is strictly smaller than the quadratic scale ε_max²/2. Weak-field Regge and continuum-limit arguments on the RS cubic lattice cite this to keep J-cost higher-order errors below the leading Laplacian term. The proof is two nlinarith steps from positivity and ε_max < 1.
Claim. If $0 < \varepsilon_{\max} < 1$, then $\varepsilon_{\max}^{4}/24 < \varepsilon_{\max}^{2}/2$.
background
The module proves Regge convergence on the RS cubic lattice $\mathbb{Z}^{3}$ without the full CMS regularity package. Cubes have perfect shape quality, the eight-tick period supplies a UV cutoff, and strict convexity of the J-cost supplies energy estimates.
Strategy item (c) invokes the analytic bound $|J(e^{\varepsilon})-\varepsilon^{2}/2|\le|\varepsilon|^{4}/24$ on the J-cost remainder. In the weak-field window $|\varepsilon|<\varepsilon_{\max}<1$, that remainder must sit strictly below the quadratic leading term so it cannot spoil $O(a^{2})$ lattice convergence. The present inequality is the elementary comparison that makes that claim quantitative at a single site; summing over $N\sim V a^{-3}$ sites then yields a total error $O(a)$ that vanishes as $a\to 0$.
proof idea
From $0<\varepsilon_{\max}<1$, nlinarith gives $\varepsilon_{\max}^{2}<1$. A second nlinarith call, feeding nonnegativity of $\varepsilon_{\max}^{2}$ and of $\varepsilon_{\max}^{4}$, rearranges to $\varepsilon_{\max}^{4}/24 < \varepsilon_{\max}^{2}/2$. No external lemmas beyond sq_nonneg are required.
why it matters
This is the elementary gate that turns the pointwise J-cost remainder bound into a continuum-safe error estimate on the RS lattice. Module strategy (d) needs exactly this comparison: once the quartic is dominated by the quadratic scale for $|\varepsilon|<\varepsilon_{\max}<1$, the correction is $O(a^{4})$ per site and $O(a)$ globally, so it does not disturb the $O(a^{2})$ Lax-type convergence of the lattice Laplacian action. Downstream siblings (weak-field error estimate, weak-field convergence, RS cubic convergence conditions) sit on top of this comparison even though the dependency graph has not yet wired them. Framework-wise it supports the continuum limit of the Recognition Composition Law cost $J$ on the eight-tick cubic lattice without invoking CMS aspect-ratio hypotheses.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.