regime_covered
plain-language theorem explainer
regime_covered classifies each gravitational perturbation regime by certification status under the nonlinear Regge framework. It returns true precisely for the linearized and weak-field cases, false otherwise. Observational astrophysicists checking coverage of solar-system tests or gravitational-wave signals cite this map when verifying that the linearized regime suffices. The definition proceeds by exhaustive case analysis on the four constructors of the ConvergenceRegime inductive type.
Claim. Define the function $C : R → {⊤, ⊥}$ on the set of regimes $R = {linearized, weakField, strongField, ultraStrong}$ by $C(linearized) = C(weakField) = ⊤$ and $C(strongField) = C(ultraStrong) = ⊥$, where linearized corresponds to $|h_{μν}| ≪ 1$ and weakField to $|h_{μν}| < 0.1$.
background
The module NonlinearReggeProof examines whether Regge calculus converges in the nonlinear regime for gravity. ConvergenceRegime is the inductive type with constructors linearized (|h| << 1), weakField (|h| < 0.1), strongField (|h| ~ O(1)), and ultraStrong (|h| >> 1). The module document states that the linearized regime is fully certified in CubicReggeProof.lean while the nonlinear regime requires the Cheeger-Muller-Schrader theorem for regularity on piecewise-linear manifolds. The φ-lattice supplies the needed uniform edge lengths automatically.
proof idea
The definition is implemented by pattern matching on the inductive type ConvergenceRegime. It assigns true to the linearized and weakField constructors and false to strongField and ultraStrong.
why it matters
This definition supplies the coverage predicate used by linearized_covers_observational to confirm that solar-system, galaxy-rotation, and gravitational-wave regimes are covered. It also supports the theorem linearized_implies_weak. In the module's regime table it marks the first four observational regimes as covered while leaving black-hole interiors open, consistent with the RS path that relies on the φ-lattice for CMS regularity conditions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.