ForecastTimescale
plain-language theorem explainer
ForecastTimescale enumerates the five canonical forecast horizons used in Recognition Science climate modeling. Operational forecasters cite it when certifying skill decay by the inverse golden ratio across successive horizons on the phi-ladder. The declaration is a plain inductive type with five constructors that derives Fintype, enabling immediate cardinality verification by decision procedures.
Claim. Let $T$ be the finite set of forecast timescales consisting of the five elements short-range, medium-range, extended-range, monthly, and seasonal, equipped with decidable equality and finite type structure.
background
The Climate Forecast Skill from J-Cost module models operational weather and climate forecast accuracy via J-cost decay on the phi-ladder. It records that adjacent horizon skill ratios approximate $1/φ$, with the Lorenz predictability limit near 15 days, and introduces five canonical timescales to match configDim $D=5$. This inductive definition supplies the discrete set required for the certification theorems that follow.
proof idea
The declaration is an inductive type definition introducing five named constructors. It attaches derivations for DecidableEq, Repr, BEq, and Fintype to support automatic equality decisions and finite cardinality computations. No further tactics or lemmas are invoked.
why it matters
ForecastTimescale supplies the finite enumeration required by the ClimateForecastCert structure, which asserts Fintype.card $T=5$, strictly positive skill values, decay ratio $φ^{-1}$, and Lorenz limit of 15 days. It operationalizes the phi-ladder prediction for climate forecasting inside the Recognition Science framework, where skill decay follows from the Recognition Composition Law.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.