CoronalTimescale
plain-language theorem explainer
CoronalTimescale enumerates the five solar corona timescales aligned to the phi-ladder in Recognition Science. Solar physicists modeling MHD events would cite the type when matching observed durations to self-similar ratios. The declaration is a plain inductive definition that automatically derives decidable equality, representation, boolean equality, and finite cardinality.
Claim. The type of coronal timescales is defined inductively by the five constructors for Alfvén crossing time, granulation convection time, chromospheric evaporation time, coronal loop lifetime, and active region lifetime.
background
Recognition Science places solar corona phenomena on the phi-ladder, where adjacent timescales differ by powers of the golden ratio phi arising from the self-similar fixed point. The module lists five specific timescales spanning five decades: Alfvén crossing near 10 s, granulation near 600 s, chromospheric evaporation near 6000 s, coronal loop near 60000 s, and active region near 600000 s. This setup follows the forcing chain T5-T6 that forces phi and the Recognition Composition Law that governs multiplicative relations.
proof idea
CoronalTimescale is introduced directly as an inductive type with exactly five constructors. The deriving clauses equip the type with DecidableEq, Repr, BEq, and Fintype without additional lemmas or tactics.
why it matters
The definition supplies the finite set whose cardinality equals 5 and whose adjacent ratios equal phi, as certified by the downstream structure CoronalTimescaleCert and the theorem coronalTimescaleCount. It fills the B12 solar depth by enumerating the timescales that must obey the phi-ratio condition. The five-decade span extends the configDim D = 5 for temporal phenomena, consistent with the spatial D = 3 fixed at T8.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.