alfvenToSolarWindRatio_gt_one
plain-language theorem explainer
The theorem shows that the Alfvén-to-solar-wind speed ratio, defined as the cube of the golden ratio, exceeds unity. Solar-wind modelers working in recognition dynamics cite it to confirm the outflow multiplier is greater than one. The proof unfolds the definition then invokes the strict inequality 1 < φ together with the quadratic identity φ² = φ + 1 inside nonlinear arithmetic.
Claim. $1 < phi^3$ where $phi$ denotes the golden ratio satisfying $phi^2 = phi + 1$.
background
The module treats the solar wind as a continuous plasma outflow whose speed at 1 AU is predicted to be the coronal Alfvén speed multiplied by φ³. The definition alfvenToSolarWindRatio is exactly that multiplier φ³. Upstream lemmas supply the two facts needed for the comparison: one_lt_phi asserts 1 < φ and phi_sq_eq asserts φ² = φ + 1. The surrounding framework links this ratio to the J-cost of the kinetic-to-thermal energy partition at the Parker spiral angle.
proof idea
The term proof first unfolds alfvenToSolarWindRatio to expose φ³. It then obtains the hypothesis 1 < φ from one_lt_phi and feeds that hypothesis plus the identity phi_sq_eq together with the non-negativity of φ² into nlinarith, which discharges the goal 1 < φ³.
why it matters
The result is one of the four fields assembled into the SolarWindCert record. It directly supports the RS prediction that solar-wind speed equals Alfvén speed times φ³ and therefore sits inside the T6 self-similar fixed-point step of the forcing chain. The parent cert is the only downstream consumer; no open scaffolding remains for this inequality.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.