convergence_is_second_order
plain-language theorem explainer
For lattice spacing a in (0,1), the squared spacing satisfies a² < a. Continuum-limit and gravity certificates cite this to mark an O(a²) lattice error as genuinely second-order (strictly finer than first order on the unit interval). The proof is a one-line nonlinear-arithmetic discharge of the elementary inequality.
Claim. For every real $a$ with $0 < a < 1$, one has $a^{2} < a$.
background
The module extends the one-dimensional continuum-limit second-order result to the full D=3 product lattice Z³. On that lattice the discrete Laplacian is the sum of three independent one-dimensional second-difference operators, one per axis. Scaling by the lattice spacing a and sending a → 0 recovers the continuum Laplacian ∇² with an O(a²) remainder; that remainder is the kinetic operator of the lattice action and, for metric perturbations in harmonic gauge, becomes the linearized Ricci piece R_μν ~ ∇² h_μν.
Upstream, the J-cost of nearest-neighbor differences reduces in the quadratic (small-perturbation) regime to a lattice Laplacian: neighbor_cost(f,x) ≈ (1/2) ∑_k [(f(x+e_k)−f(x))² + (f(x−e_k)−f(x))²], which is the content of ContinuumLimit.jcost_gives_laplacian_structure. Spatial dimension is fixed at D = 3 by the forcing chain (T8).
The present inequality is the elementary comparison that turns the O(a²) error bound into a strict second-order statement whenever the spacing lies in the open unit interval.
proof idea
Term-mode proof discharged by a single nlinarith call. The hypotheses 0 < a and a < 1 immediately imply a·a < a·1, i.e. a² < a; no intermediate lemmas are required.
why it matters
The declaration is the arithmetic witness that lattice convergence is at least second order in spacing. Downstream, NonlinearConvergence.nonlinear_convergence_cert installs it as the second_order field (via a thin wrapper that re-supplies the positivity and unit-interval bounds by linarith). That certificate, together with the CMS bulk-vanishing bounds, feeds the full GR certificate in Gravity.FullEFE, which packages dimension, derived κ, positivity, and conservation for the Recognition-Science Einstein equation.
In the broader framework this sits under the D = 3 forcing (T8) and the continuum limit of the J-cost kinetic term: once the lattice Laplacian converges at O(a²), the linearized curvature operator is under control and the continuum GR limit can be certified rather than postulated. The sibling NonlinearConvergence.convergence_is_second_order records the same rate under a stronger quadratic hypothesis; the present lemma is the shared elementary engine.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.