solarWindTypeCount
plain-language theorem explainer
The result establishes that the inductive enumeration of solar wind configurations contains exactly five elements. Astrophysicists applying Recognition Science to magnetohydrodynamic flows cite this cardinality to anchor the discrete classification of observed speed bands. The proof is a one-line decide tactic that evaluates the Fintype instance generated by the five constructors.
Claim. The finite set of solar wind types, consisting of the elements quiet, slow, intermediate, fast, and extreme, has cardinality five: $|S| = 5$ where $S$ denotes this set.
background
The module treats solar wind as an instance of the phi-ladder in B12 astrophysical MHD. SolarWindType is defined inductively with five constructors (quiet, slow, intermediate, fast, extreme) and automatically derives Fintype, DecidableEq, and related instances. The module document states that this count equals the configuration dimension D = 5, consistent with the three canonical speed bands plus intermediate and quiet regimes whose ratios approximate powers of phi.
proof idea
The proof is a one-line wrapper that applies the decide tactic directly to the cardinality equality. The tactic succeeds because the inductive type derives Fintype, allowing Lean to reduce the statement to a finite enumeration over the five constructors.
why it matters
The theorem supplies the five_types component of the solarWindCert certificate, which pairs the count with the phi speed ratio. It completes the discrete classification step required by the module's claim that configDim D = 5 follows from the phi-ladder. The result sits downstream of the inductive definition and feeds the certificate used to record the RS prediction for solar wind structure.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.