coronalTime_succ_ratio
plain-language theorem explainer
The coronal timescale on the phi-ladder obeys the recurrence τ(k+1) = φ · τ(k) for each natural number k. Solar physicists modeling chaotic field-line divergence in the corona would cite this to anchor the exponential growth of Lyapunov times to the golden ratio. The proof is a one-line wrapper that unfolds the definition of coronalTime and applies the successor rule for powers followed by algebraic simplification.
Claim. For every natural number $k$, the coronal timescale at rung $k+1$ equals the coronal timescale at rung $k$ multiplied by the golden ratio $phi$.
background
The module places solar-coronal magnetic configurations on a phi-ladder of timescales, with reference timescale equal to the Alfvén crossing time. The function coronalTime is defined by coronalTime k := referenceTime * phi ^ k, so successive rungs differ by exact factors of phi. This mirrors the self-similar fixed point phi across astrophysical scales, with the upstream definition supplying the base expression for the rung-k timescale.
proof idea
This is a one-line wrapper proof. It unfolds the definition of coronalTime, rewrites the power using the successor rule, and closes with the ring tactic for algebraic simplification.
why it matters
This supplies the multiplicative step used by coronal_adjacent_ratio to prove the ratio equals phi exactly and by coronalLyapunovCert to assemble the full certificate. It fills the rung-successor step in the phi-ladder for coronal Lyapunov times, aligning with the self-similar fixed point phi in the forcing chain. The module provides a falsifier based on measured ratios outside the interval (1.5, 1.8).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.