linearized_implies_weak
plain-language theorem explainer
The declaration shows that certification of the linearized gravitational regime entails certification of the weak-field regime under the Recognition Science convergence map. Researchers verifying Regge calculus approximations across perturbation orders would reference this link when building regime chains. The proof reduces immediately to the case analysis in the definition of regime_covered via a decision procedure.
Claim. If the convergence coverage function returns true on the linearized regime, then it returns true on the weak-field regime.
background
The module examines whether strong-field Regge convergence can be proved to close the black-hole interior gap. The convergence coverage function is defined by case analysis on four regimes: it returns true for linearized and weak-field, false for strong-field (pending CMS regularity) and ultra-strong (open). The module table lists physical scales with |h_μν| from 10^{-21} to O(1), marking linearized as covered and strong-field as conditional on the Cheeger-Muller-Schrader theorem for piecewise-linear manifolds.
proof idea
The proof is a one-line wrapper that applies the decide tactic to the definition of the convergence coverage function, confirming both input regimes evaluate to true.
why it matters
This result bridges the linearized and weak-field regimes in the Nonlinear Regge Convergence analysis, confirming coverage for solar-system through gravitational-wave scales without CMS. It fills the lower half of the regime table in the module and supports the RS path that the φ-lattice supplies automatic regularity for weak perturbations. The open question it touches is closure of the strong-field and black-hole interior cases.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.