rotationRegime_count
plain-language theorem explainer
The theorem fixes the cardinality of the rotation regime type at five, enumerating the canonical regimes in RS-derived galactic dynamics. Astrophysicists working with rotation curve models cite it to anchor the configDim at five. The proof is a one-line decision tactic that exhausts the finite inductive constructors.
Claim. The finite type of galactic rotation regimes has cardinality five: $|RotationRegime| = 5$.
background
The module partitions galactic rotation curves into five regimes: rigid-body inner, rising, flat (MOND or dark matter), declining, and truncation. These are the constructors of the inductive type RotationRegime, which automatically derives Fintype. The module states that transition radii lie one rung up the phi-ladder and sets configDim equal to five.
proof idea
The proof is a one-line wrapper that applies the decide tactic to compute the cardinality by enumerating the five constructors of the inductive type RotationRegime.
why it matters
This supplies the five_regimes field inside galacticRotationCert, which certifies the full rotation curve model. It implements the five-regime count asserted in the module documentation. The result aligns with the framework's finite configuration dimensions, here specialized to five for rotation regimes.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.