solarWindSpeedRatio
plain-language theorem explainer
Consecutive solar wind speeds defined on the phi-ladder obey the constant ratio phi. Researchers modeling solar wind in the Recognition Science framework cite this result to recover the approximate factor of 2 between slow and fast wind bands from the self-similar structure. The argument consists of unfolding the power definition of solarWindSpeed and reducing the ratio via the ring tactic after a positivity check.
Claim. For every natural number $k$, the ratio of solar wind speed at rung $k+1$ to the speed at rung $k$ equals the golden ratio $phi$.
background
The module Solar Wind from Phi-Ladder models solar wind speeds via the phi-ladder construction in Recognition Science. The definition solarWindSpeed k := phi^k places the sequence on successive rungs, with the five canonical types (slow, fast, intermediate, extreme, quiet) corresponding to configDim D = 5. This yields the prediction that the slow-to-fast ratio approximates phi, as noted in the module documentation.
proof idea
The proof unfolds solarWindSpeed to obtain phi^{k+1} divided by phi^k. It introduces the fact pow_pos phi_pos k to establish that the denominator is nonzero, rewrites the division using div_eq_iff, and simplifies the resulting equation with the ring tactic.
why it matters
This declaration provides the phi_ratio component of the solarWindCert structure, which packages the five wind types together with the ratio identity. It realizes the RS prediction stated in the module that slow/fast wind ratio ≈ phi, aligning with the phi-ladder and the forcing chain landmarks T6 and T7. The result closes the algebraic step needed for the astrophysical certification without introducing open scaffolding.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.