solarWindCert
plain-language theorem explainer
The solarWindCert definition assembles a certificate verifying exactly five solar wind types with consecutive speeds in fixed ratio phi. Astrophysicists modeling solar wind bands would cite it to embed the phi-ladder prediction into Recognition Science derivations. The construction is a direct record of two prior theorems establishing the type count by decision and the ratio by algebraic simplification.
Claim. Define the solar wind certificate as the record whose fields satisfy that the cardinality of solar wind types equals 5 and that the ratio of successive solar wind speeds equals the golden ratio φ for every natural number k.
background
Recognition Science places solar wind speeds on the phi-ladder, with the module predicting a constant ratio of consecutive speeds equal to φ. The local setting states three canonical bands (slow ~300-400 km/s, fast ~600-800 km/s, extreme >1000 km/s) and asserts that the five canonical types (slow, fast, intermediate, extreme, quiet) equal configDim D = 5. Upstream, the type-count theorem confirms the cardinality by direct decision while the speed-ratio theorem derives the equality by unfolding the speed definition and applying ring simplification.
proof idea
The definition is a one-line wrapper that supplies the five_types field directly from the type-count theorem and the phi_ratio field directly from the speed-ratio theorem.
why it matters
This definition completes the phi-ladder certificate for solar wind, supplying the structure required by the B12 astrophysical MHD step. It directly encodes the RS prediction that the slow/fast wind ratio approximates φ and closes the scaffolding for the five-type count and constant-ratio properties. No downstream theorems are listed, so the declaration stands as the terminal record for these two facts.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.