Astrophysics Solar Wind From Phi Ladder Solar Wind Speed Ratio

The speed ratio

The solar wind is a stream of charged particles flowing from the Sun's outer atmosphere. Spacecraft measurements have long separated it into speed bands: slow wind near 300 to 400 kilometers per second, fast wind near 600 to 800, and extreme events like coronal mass ejections above 1000. The ratio of fast to slow wind is roughly two to one, a number close to the golden ratio, about 1.618, raised to a power.

In the Recognition Science framework, the solar wind appears as a ladder of speeds. The framework defines a sequence where each rung's speed is the golden ratio times the previous rung's speed. A theorem in the framework's machine-checked library of formal theorems proves that the ratio of consecutive speeds equals the golden ratio exactly. The proof is a short algebraic identity: if each speed is the golden ratio raised to an integer power, then dividing one by its predecessor cancels everything except the ratio itself.

The same library also defines five solar wind types: quiet, slow, intermediate, fast, and extreme. A second theorem proves that the count of these types is five. Both facts are packaged into a certificate structure, which bundles the five-type count and the ratio law into one object. The certificate is built from the two theorems, so it inherits their machine-checked status.

What the declaration does not claim is where the honesty lies. The theorem proves a relationship between speeds in the framework's model, not a measurement of the actual solar wind. The observed fast-to-slow ratio of about two is a physical fact, not a consequence of the theorem. The framework's choice to place solar wind speeds on a golden ratio ladder is a modeling decision, not a derivation from solar physics. The theorem guarantees that if you accept the model's definition of speeds, the ratio follows; it does not guarantee that the model matches the Sun.

The practical consequence is modest but real. The framework offers a compact way to encode the observed two-to-one speed ratio as an exact mathematical structure. Whether that structure explains why the wind has the speeds it does remains a question for observation and further theory, not for the theorem itself.

theorem solarWindSpeedRatio (k : ℕ) :
    solarWindSpeed (k + 1) / solarWindSpeed k = phi := by
  unfold solarWindSpeed
  have hpos := pow_pos phi_pos k
  rw [pow_succ, div_eq_iff hpos.ne']
  ring

theorem solarWindTypeCount : Fintype.card SolarWindType = 5 := by decide

noncomputable def solarWindCert : SolarWindCert where
  five_types := solarWindTypeCount
  phi_ratio := solarWindSpeedRatio

What this page does not claim

The theorem does not measure the solar wind's actual speed. The observed fast-to-slow ratio of about two is not derived from the framework. The choice to model speeds on a golden ratio ladder is not a derivation from solar physics.

Verify this page

Every tagged claim above names its theorem. To check one yourself rather than trust this page, elaborate the source module with Lean 4 and audit its axiom basis:

$ lake env lean IndisputableMonolith/Astrophysics/SolarWindFromPhiLadder.lean
expected axiom basis: [propext, Classical.choice, Quot.sound] (the Lean kernel's standard three; no RS-specific axioms)

A page whose claims cannot be reproduced this way does not ship. In production, every anchor links to the exact declaration in the public source release, and this block carries the build receipt for the page itself.

Derived articles

This page is generated by a question-recursion engine: the questions its answers raise become the next pages. The current agenda, with open targets marked red: