ConvergenceRegime
plain-language theorem explainer
ConvergenceRegime supplies an inductive classification of four metric-perturbation regimes for nonlinear Regge calculus, keyed to the size of |h_μν|. Strong-field gravity and black-hole researchers cite it when mapping observational coverage onto the φ-lattice. The declaration is a pure inductive enumeration whose constructors carry only magnitude comments.
Claim. An inductive type whose constructors label convergence regimes by metric-perturbation strength: linearized when $|h|ll 1$, weakField when $|h|<0.1$, strongField when $|h|sim O(1)$, and ultraStrong when $|h|gg 1$.
background
The module addresses Nonlinear Regge Convergence (Q12) on the φ-lattice whose edge lengths are uniform multiples of the backbone scale φ²×1.47. This lattice structure is asserted to satisfy the regularity hypotheses of the Cheeger-Muller-Schrader theorem automatically. ConvergenceRegime enumerates the four regimes that decide whether the linearized approximation is sufficient or whether the full nonlinear CMS conditions must be invoked.
proof idea
The declaration is an inductive definition introducing four constructors, each annotated with a magnitude comment on |h_μν|. No lemmas or tactics are invoked; the type is used directly by the downstream function regime_covered.
why it matters
The definition is the immediate input to regime_covered, which returns true precisely for the linearized and weakField cases. It therefore marks the boundary between the fully certified linearized regime (already proved in CubicReggeProof) and the conditional strong-field cases that still require the CMS regularity argument on the φ-lattice. The classification directly populates the module's coverage table for solar-system, galactic, and black-hole regimes.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.