coronalTimescaleCount
plain-language theorem explainer
The declaration establishes that the inductive type enumerating coronal timescales contains exactly five elements. Astrophysicists working within the Recognition Science framework would cite it when counting the discrete timescales on the phi-ladder for solar corona modeling. The proof is a one-line decision procedure that evaluates the finite type cardinality directly from the inductive definition.
Claim. The finite set of coronal timescales has cardinality five: $ |C| = 5 $, where $C$ consists of the Alfvén crossing time, granulation convection, chromospheric evaporation, coronal loop lifetime, and active region lifetime.
background
The module lists five coronal timescales on the phi-ladder with approximate values: Alfvén crossing (~10 s), granulation convection (~600 s), chromospheric evaporation (~6000 s), coronal loop lifetime (~60000 s), and active region lifetime (~600000 s). These span five decades with adjacent-step ratios near 10, matching the RS prediction of phi^k scaling and configDim D = 5. The upstream inductive definition enumerates exactly these five cases and derives Fintype, Repr, and DecidableEq to support cardinality and equality computations.
proof idea
The proof is a one-line wrapper that invokes the decide tactic on the Fintype instance automatically generated from the inductive type with five constructors.
why it matters
This supplies the five_timescales field to the downstream CoronalTimescaleCert definition, which also carries the phi_ratio from timescaleRatioPhiRung. It anchors the astrophysics section of the Recognition Science model by confirming the discrete count of timescales that follow the phi-ladder, consistent with the eight-tick octave and D = 3 spatial dimensions extended to configDim = 5 decades. The module records zero sorry and zero axiom for the entire file.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.