SolarWindType
plain-language theorem explainer
The solar wind type enumeration defines five discrete regimes for solar wind speeds within the Recognition Science phi-ladder model. Astrophysicists studying magnetohydrodynamic flows would cite this enumeration when establishing the basis for speed ratio predictions. The declaration proceeds by listing the five constructors and automatically deriving decidable equality along with finite type structure.
Claim. Define the inductive type $T$ of solar wind classifications with constructors quiet, slow, intermediate, fast, extreme. The type carries decidable equality and forms a finite set of cardinality 5.
background
The module sets up solar wind classification inside the phi-ladder framework of Recognition Science. It distinguishes five types (quiet, slow, intermediate, fast, extreme) that realize configDim D = 5, with the prediction that adjacent speeds satisfy the ratio phi. Canonical bands are given as slow wind 300-400 km/s and fast wind 600-800 km/s. The declaration imports only Mathlib and Constants; no upstream lemmas are invoked.
proof idea
The declaration is a direct inductive definition that enumerates the five cases and derives the instances DecidableEq, Repr, BEq, Fintype via the deriving clause.
why it matters
This enumeration supplies the carrier type for the SolarWindCert structure, which asserts both cardinality 5 and the phi ratio on adjacent speeds. It realizes the five canonical solar wind types stated in the module documentation for B12 Astrophysical MHD. The construction supports the Recognition Science claim that solar wind speed ratios approximate phi, consistent with the self-similar fixed point.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.