coronalTime_pos
plain-language theorem explainer
The result shows that the coronal Lyapunov timescale at every rung k of the phi-ladder is positive. Solar physicists constructing models of magnetic reconnection and field-line divergence would invoke this positivity to guarantee well-defined timescales. The proof reduces the claim to the known positivity of phi raised to k by unfolding the definitions of coronalTime and referenceTime, then closes with linear arithmetic.
Claim. For every natural number $k$, the coronal timescale at rung $k$ given by $1 · ϕ^k$ satisfies $0 < 1 · ϕ^k$.
background
The module places solar-coronal magnetic-field evolution on the phi-ladder of characteristic timescales. Reference timescale is the Alfvén crossing time fixed at 1 in RS-native units. Coronal timescale at rung k is defined as referenceTime multiplied by phi to the power k, where phi is the golden-ratio fixed point supplied by the upstream Constants structure.
proof idea
The term proof unfolds coronalTime and referenceTime to reach the expression 1 * phi ^ k. It applies pow_pos using Constants.phi_pos to obtain 0 < phi ^ k, then invokes linarith to finish.
why it matters
This positivity is required by the downstream coronalLyapunovCert bundle and by the adjacent-ratio and strictly-increasing theorems. It anchors the coronal rung of the phi-ladder (T6 phi fixed point, T7 eight-tick octave) inside the Recognition framework, ensuring all predicted Lyapunov times remain positive before reconnection.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.