RotationRegime
plain-language theorem explainer
RotationRegime enumerates the five canonical regimes of galactic rotation curves in Recognition Science: rigid-body inner, rising, flat, declining, and truncation. Astrophysicists deriving curves from the phi-ladder cite it to certify the exact count and ordering of regimes. The declaration is a direct inductive type that derives Fintype for immediate cardinality checks in downstream structures.
Claim. An inductive type whose five constructors label the regimes of a galactic rotation curve: rigid-body inner, rising, flat, declining, and truncation.
background
The Astrophysics.GalacticRotationCurveFromRS module decomposes galactic rotation curves into five regimes that match configDim D = 5. The regimes are rigid-body inner, rising, flat (linked to MOND or dark-matter interpretations), declining, and truncation, with each transition radius placed one rung higher on the phi-ladder. The module records zero sorry and zero axiom, confirming a complete formalization inside the Recognition Science setting.
proof idea
The declaration is a direct inductive definition that introduces the five constructors and derives DecidableEq, Repr, BEq, and Fintype. No lemmas are applied; the Fintype instance is generated automatically to support cardinality theorems.
why it matters
This definition supplies the five-regime enumeration required by the GalacticRotationCert structure, which asserts Fintype.card RotationRegime = 5 together with the phi-ratio property on transition radii. It realizes the D = 5 decomposition stated in the module, where the flat regime corresponds to the MOND/DM regime and transitions follow the phi-ladder. The construction closes the regime-count step that feeds rotation-curve certification.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.