timescaleRatioPhiRung
plain-language theorem explainer
Consecutive timescales on the phi-ladder differ by the exact factor phi. Solar MHD modelers would cite this to connect Alfvén times to active-region lifetimes via the Recognition Science ladder. The proof is a direct algebraic reduction after substituting the definition of timescaleAtRung as phi to the power k.
Claim. For every natural number $k$, the ratio of the timescale at rung $k+1$ to the timescale at rung $k$ equals the golden ratio phi, where the timescale at rung $k$ is defined as phi raised to the power $k$.
background
The module constructs solar corona timescales from the phi-ladder in solar MHD. It lists five characteristic times: Alfvén crossing near 10 s, granulation convection near 600 s, chromospheric evaporation near 6000 s, coronal loop lifetime near 60000 s, and active region lifetime near 600000 s. These span five decades, with the RS prediction that adjacent steps maintain a constant ratio given by powers of phi. The upstream definition assigns the timescale at rung k explicitly as phi to the power k.
proof idea
The proof unfolds the definition of timescaleAtRung on both sides to obtain phi to the power k+1 over phi to the power k. It applies pow_pos to establish positivity of phi to the power k, rewrites the division via div_eq_iff, and finishes with the ring tactic to cancel the common factor.
why it matters
This theorem supplies the phi_ratio field inside coronalTimescaleCert, which bundles the five timescales with their scaling relation. It realizes the module's prediction of constant phi ratios across the ladder, connecting directly to the self-similar fixed point phi from the forcing chain. The result closes the scaling step required for the certificate.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.