linearized_covers_observational
plain-language theorem explainer
This definition asserts that the linearized and weak-field regimes together cover all current observational tests of gravity. It would be cited by researchers verifying that solar-system, galaxy-rotation, and gravitational-wave data fall inside the certified domain of the phi-lattice Regge model. The body is a direct conjunction of the two boolean flags supplied by the regime classification.
Claim. The boolean predicate that the linearized regime together with the weak-field regime suffices for observational coverage holds precisely when both flags evaluate to true.
background
The module classifies convergence regimes via ConvergenceRegime with four cases: linearized, weakField, strongField, and ultraStrong. The upstream definition regime_covered maps the first two cases to true and the latter two to false pending the Cheeger-Muller-Schrader theorem on piecewise-linear manifolds. Module documentation states that the phi-lattice supplies uniform edge lengths that automatically meet CMS regularity conditions, thereby covering solar-system (|h_μν| ~ 10^{-6}), galaxy (~10^{-4}), wave (~10^{-21}), and CMB (~10^{-5}) regimes while leaving neutron-star and black-hole regimes conditional.
proof idea
The definition is a one-line wrapper that applies regime_covered to the linearized case, applies it again to the weakField case, and returns their conjunction.
why it matters
The definition supplies the linearized_sufficient field inside the NonlinearReggeCert structure and is invoked by the theorem observational_regime_covered. It therefore certifies that all presently accessible gravitational tests lie inside the Recognition Science phi-lattice coverage, closing the weak-field half of the Q12 question while the strong-field half remains open pending CMS. The module table explicitly lists the linearized regime as YES and the black-hole interior as OPEN.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.