linearized_convergence_proved
plain-language theorem explainer
Defines the proposition that the centered second finite-difference of a C^4 real function converges to its second derivative with an O(a^2) remainder. Gravity and continuum-limit workers cite it as the precise statement of linearized lattice-to-continuum convergence (Axiom 1 in the weak-field regime). It is a bare Prop definition; the witness is supplied by the sibling error-estimate theorem.
Claim. For every $C^4$ map $f:\mathbb{R}\to\mathbb{R}$ and all $x,a\in\mathbb{R}$ with $a\neq 0$, there exists $C\ge 0$ such that $\bigl|\frac{f(x+a)+f(x-a)-2f(x)}{a^2}-f''(x)\bigr|\le C\,a^2$.
background
The module proves that the Regge action on the Recognition Science lattice converges to the Einstein-Hilbert action in the continuum limit. Convergence is split into two regimes: an unconditional linearized (weak-field) regime, and a conditional full nonlinear regime under Cheeger-Muller-Schrader-type hypotheses.
In the linearized chain, the J-cost expands as $\cosh(\varepsilon)-1=\varepsilon^2/2+O(\varepsilon^4)$; the quadratic sum becomes a lattice Laplacian action; that Laplacian, scaled by $a^{-2}$, converges to $\nabla^2$ at $O(a^2)$; and in Newtonian gauge $\nabla^2\Phi$ is the Ricci scalar, so the action matches linearized EH. The present definition isolates the analytic core of step 3: second-difference to second-derivative with a concrete $O(a^2)$ bound for $C^4$ test functions.
Sibling material in the same file packages the proved instance (linearized_convergence) and a certificate that weak-field scope covers solar-system through GW amplitudes.
proof idea
No proof body: this is a def equating a name to a Prop. The quantified statement is the standard Taylor remainder for the centered second difference under four continuous derivatives. Discharge is deferred to linearized_error_estimate, which linearized_convergence applies as a one-line wrapper to inhabit this proposition.
why it matters
Marks the precise content of Axiom 1 in the linearized case: Regge on $\mathbb{Z}^3$ equals the lattice Laplacian action and converges to continuum EH at $O(a^2)$. Downstream, FullDerivationChain records it as step4_variational_limit; ReggeConvergenceCert requires linearized_ok : linearized_convergence_proved and notes sufficiency for solar system ($|h|\sim 10^{-6}$), galaxy rotation, CMB, and gravitational waves. FullGRCertificate / FullGRCertificateV2 sit on the same RS-to-GR spine (J-cost quadratic, Regge from J, $\kappa=8\varphi^5$, discrete Bianchi). The nonlinear CMS route remains conditional; this Prop closes only the weak-field half of the module strategy.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.