linearized_convergence
plain-language theorem explainer
In the weak-field regime the Regge action on the RS lattice converges to the continuum Einstein-Hilbert (Laplacian) action at order O(a²) in mesh size. Continuum-limit and RS-gravity workers cite this as the unconditional half of lattice-to-GR convergence. The proof is a one-line appeal to the linearized error estimate already established in the module.
Claim. The linearized Regge-to-continuum convergence claim holds: in the weak-field limit $h \ll 1$, the discrete Regge action on the RS lattice converges to the continuum Einstein-Hilbert action with an $O(a^2)$ error bound in the mesh size $a$.
background
This module establishes that the Regge action built on the Recognition Science lattice converges to the Einstein-Hilbert action in the continuum limit. Convergence is split into two regimes. The linearized (weak-field) regime is unconditional; the full nonlinear regime is only conditional on stronger shape and curvature hypotheses that are not the general Cheeger-Muller-Schrader package.
In the weak-field limit the metric perturbation satisfies $h \ll 1$, so the Regge action reduces to a lattice Laplacian action. That discrete Laplacian is already known (via the continuum-limit infrastructure) to approach the continuum Laplacian at order $O(a^2)$ in the mesh size $a$. The present declaration packages that fact as the named linearized-convergence proposition used by the rest of the gravity stack.
The module strategy notes that this linearized case already covers the practical RS-gravity applications: solar-system tests, galaxy rotation, and cosmological perturbation theory. Strong-field and black-hole interiors are deferred to the conditional nonlinear statements.
proof idea
One-line term proof: the goal is definitionally the proposition linearized_convergence_proved, and the term supplied is the already-proved linearized error estimate. No extra tactics or algebraic rewriting appear; the declaration is a named alias that re-exports that estimate as the module's linearized-convergence theorem.
why it matters
The module header frames this result as the proved half of "Regge Convergence: Lattice to Einstein (Proves Axiom 1)". Downstream, regge_convergence_cert records linearized_ok by direct appeal to this theorem, and the FullEFE certificates (full_gr_certificate, FullGRCertificate, full_gr_certificate_v2, rs_derivation_chain) treat Regge-from-J-cost plus continuum recovery as steps on the RS-to-GR chain.
In framework terms it closes the lattice-to-continuum bridge for the weak-field sector that RS gravity actually uses for phenomenology. The nonlinear CMS-style envelope remains conditional; this declaration deliberately does not claim that stronger regime, keeping the unconditional certificate honest.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.