coronalTimescaleCount
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.
claimThe 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 in Recognition Science
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.
scope and limits
- Does not assign physical units or numerical values to the timescales.
- Does not prove that adjacent ratios equal phi to an integer power.
- Does not link the count to the forcing chain T0-T8 or the Recognition Composition Law.
- Does not address stability or observability of the listed timescales.
Lean usage
example : Fintype.card CoronalTimescale = 5 := coronalTimescaleCountformal statement (Lean)
29theorem coronalTimescaleCount : Fintype.card CoronalTimescale = 5 := by decide
proof body
30