SolarWindCert
plain-language theorem explainer
The structure SolarWindCert packages the assertion that exactly five solar wind regimes exist and that consecutive speeds on the phi-ladder stand in the golden ratio. Recognition Science derivations of astrophysical MHD cite this structure when mapping the abstract ladder to observed solar wind bands. It is introduced as a plain structure definition that directly assembles the Fintype cardinality of the five-type enumeration with the geometric ratio property of solarWindSpeed.
Claim. Let $S$ be the inductive type with constructors quiet, slow, intermediate, fast, extreme. Let $v(k) = phi^k$ denote solar wind speed at rung $k$ of the phi-ladder. The structure SolarWindCert asserts that the cardinality of $S$ equals 5 and that $v(k+1)/v(k) = phi$ for every natural number $k$.
background
In the Solar Wind from Phi-Ladder module, solar wind is modeled directly on the phi-ladder. The inductive type SolarWindType enumerates the five regimes quiet, slow, intermediate, fast, extreme and carries a Fintype instance. The function solarWindSpeed is defined by solarWindSpeed k := phi ^ k, so the ratio property holds by direct computation. The module doc states that RS predicts five canonical types matching configDim D = 5 and that the slow-to-fast speed ratio approximates phi.
proof idea
The structure is introduced by two fields only: the cardinality equality five_types drawn from the Fintype instance on SolarWindType and the universal quantification phi_ratio that follows immediately from the definition solarWindSpeed k := phi ^ k. No lemmas or tactics are invoked; the definition simply packages these two properties.
why it matters
SolarWindCert supplies the phi-ladder certificate instantiated as solarWindCert and then used to construct the MHD certificate in SolarWindFromMHD. It fills the B12 astrophysical step that derives five solar wind types with phi-ratio speeds from the self-similar fixed point (T6). The structure feeds cert_inhabited, which establishes nonemptiness of the full MHD certificate, and thereby connects the abstract phi-ladder to concrete solar wind observations.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.