CoronalLyapunovCert
plain-language theorem explainer
CoronalLyapunovCert bundles four properties of the coronal timescale function: positivity for every natural number rung, exact multiplication by phi on each step, strict increase, and adjacent ratio exactly equal to phi. Solar physicists modeling magnetic reconnection and field-line divergence in the corona would cite the certificate when checking that observed Lyapunov times sit on the predicted phi-ladder. The declaration is a bare structure definition with no attached proof obligations or computational body.
Claim. A structure whose fields assert that the coronal timescale function satisfies: for all $k$, $0 < t(k)$; for all $k$, $t(k+1) = t(k)·ϕ$; for all $k$, $t(k) < t(k+1)$; and for all $k$, $t(k+1)/t(k) = ϕ$, where $t(k)$ denotes the coronal timescale at phi-ladder rung $k$.
background
The module places solar-coronal Lyapunov times on the phi-ladder of characteristic timescales. The upstream definition coronalTime(k) sets the rung-$k$ value to referenceTime multiplied by phi to the power $k$, with referenceTime the Alfvén crossing time. MODULE_DOC states that adjacent rungs differ by exactly phi, matching the self-similar fixed point and the Recognition Composition Law that forces the eight-tick octave structure across solar, stellar, and astrophysical scales.
proof idea
The declaration is a structure definition whose four fields are simply declared as propositions; no tactics or lemmas are applied inside the declaration itself.
why it matters
The structure supplies the type that coronalLyapunovCert instantiates by supplying the four lemmas coronalTime_pos, coronalTime_succ_ratio, coronalTime_strictly_increasing and coronal_adjacent_ratio. It thereby records that the coronal Lyapunov timescale obeys the phi-ladder required by T6 (phi forced as self-similar fixed point) and T7 (eight-tick octave) of the UnifiedForcingChain. The module DOC_COMMENT gives the concrete falsifier: measured adjacent ratios lying systematically outside (1.5, 1.8) on a corpus of at least three active regions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.