coronalTimescaleCert
plain-language theorem explainer
This definition constructs a certificate that exactly five coronal timescales exist and form a ladder with consecutive ratios equal to the golden ratio phi. Solar physicists modeling MHD processes in the corona would cite it to embed observed timescales in the Recognition Science phi-ladder. The definition is assembled by directly supplying the cardinality theorem and the ratio theorem to the two fields of the certificate structure.
Claim. A certificate asserting that the set of coronal timescales has cardinality 5 and that the ratio of the timescale at rung $k+1$ to the timescale at rung $k$ equals the golden ratio $phi$ for every natural number $k$.
background
The module places solar corona timescales on the phi-ladder, listing five concrete intervals: Alfvén crossing time 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 adjacent ratios near 10, identified with powers of phi. The certificate structure requires two properties: the set contains exactly five elements, and consecutive rungs satisfy the constant ratio phi.
proof idea
The definition is a direct construction that populates the five_timescales field with the result of the cardinality theorem and the phi_ratio field with the result of the ratio theorem.
why it matters
The certificate formalizes the Recognition Science claim that coronal timescales lie on the phi-ladder, consistent with the self-similar fixed point phi derived from J-uniqueness. It supplies a modular interface for applying the phi-ladder to astrophysical data, though no downstream theorems yet depend on it.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.