CoronalTimescaleCert
plain-language theorem explainer
CoronalTimescaleCert records that the solar corona admits exactly five enumerated timescales whose consecutive ratios equal the golden ratio phi. Solar physicists applying the Recognition Science phi-ladder to MHD processes would cite this certificate when anchoring observed intervals from Alfvén crossing to active-region lifetimes. The declaration is realized as a bare structure definition that directly assembles the Fintype cardinality of the inductive enumeration with the universal ratio property of timescaleAtRung.
Claim. Let $T$ be the inductive type whose five constructors are the Alfvén crossing time, granulation convection time, chromospheric evaporation time, coronal loop lifetime, and active region lifetime. Then CoronalTimescaleCert is the structure whose fields assert $|T|=5$ and, writing $τ(k):=φ^k$, that $τ(k+1)/τ(k)=φ$ for every natural number $k$.
background
The module treats solar corona timescales as instances of the phi-ladder in Recognition Science. The inductive type CoronalTimescale enumerates the five physical regimes: alfvenCrossing, granulation, chromosphericEvaporation, coronalLoop, and activeRegion. The supporting definition timescaleAtRung (k : ℕ) : ℝ := phi ^ k supplies the rung values, while the imported phi_ratio from Quasicrystal supplies the constant 1/φ used in related ratio statements. Module documentation states that the five timescales span five decades with adjacent ratios approximately 10, consistent with φ^5 scaling.
proof idea
The declaration is a structure definition whose two fields are written directly: the first invokes Fintype.card on the CoronalTimescale inductive type, and the second states the universal quantification over the ratio of consecutive applications of timescaleAtRung. No tactics or lemmas are applied; the structure simply packages the two properties.
why it matters
The structure supplies the type for the downstream definition coronalTimescaleCert, which constructs a concrete witness using coronalTimescaleCount and timescaleRatioPhiRung. It therefore closes the B12 solar/MHD depth entry in the Recognition framework, linking observed coronal intervals to the forced self-similar fixed point phi (T6) and the eight-tick octave structure. The certificate touches the open question of whether the precise decade count D=5 follows from the spatial dimension D=3 or remains an independent input.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.