coronalTime_strictly_increasing
plain-language theorem explainer
The coronal timescale at phi-ladder rung k is strictly less than the timescale at rung k+1 for every natural number k. Solar physicists modeling magnetic reconnection and field-line divergence would cite this to confirm the ordering of characteristic coronal timescales. The proof rewrites the successor step via the ratio theorem, invokes positivity of the timescale together with phi greater than 1.5, then applies a left-multiplication inequality.
Claim. For every natural number $k$, the coronal timescale at rung $k$ is strictly less than the coronal timescale at rung $k+1$, where the timescale equals reference time times $phi^k$.
background
The module places solar coronal magnetic-field evolution on the phi-ladder of characteristic timescales, with reference time equal to one Alfvén crossing time. The coronal timescale at rung k is defined as referenceTime multiplied by phi to the power k. Upstream results establish positivity of this timescale for all k, the exact successor relation that multiplies by phi, and the bound phi greater than 1.5. The local setting ties these rungs to observed solar phenomena such as granulation, chromospheric evaporation, and active-region emergence, with adjacent rungs differing by exactly phi.
proof idea
The tactic proof first rewrites the target inequality using the successor ratio theorem. It obtains positivity of the timescale at k from the positivity theorem. A subproof derives phi greater than 1 from the phi greater than 1.5 lemma via linarith. It then applies the multiplication inequality mul_lt_mul_of_pos_left and simplifies to conclude.
why it matters
This theorem supplies the strictly_increasing component to the coronalLyapunovCert structure, which bundles positivity, one-step ratio, strict increase, and adjacent ratio equal to phi. It reinforces the phi-ladder structure in the module, consistent with the self-similar fixed point phi from the forcing chain. The result supports ordering predictions for coronal loop lifetimes and active-region emergence.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.