forecastTimescaleCount
plain-language theorem explainer
The declaration establishes that the inductive type of canonical forecast timescales contains exactly five elements. Climate researchers certifying J-cost based forecast skill bounds would cite this cardinality when populating the ClimateForecastCert structure. The proof is a one-line decision procedure that enumerates the five constructors and confirms the finite cardinality.
Claim. Let $T$ be the finite set of canonical forecast timescales consisting of the short-range, medium, extended, monthly and seasonal horizons. Then $|T| = 5$.
background
The module develops operational climate forecast skill from the J-cost functional, with skill decaying along a phi-ladder across five discrete horizons. The upstream inductive definition enumerates exactly these five cases and automatically derives the Fintype instance used for cardinality. Module documentation states that these five timescales equal the configuration dimension D = 5 and are consistent with the observed Lorenz predictability limit of roughly two weeks.
proof idea
The proof is a one-line wrapper that applies the decide tactic. This tactic evaluates the Fintype.card expression by exhaustive enumeration of the five constructors of the inductive type and returns the equality with 5.
why it matters
The result supplies the five_timescales component of the downstream climateForecastCert definition, which assembles the full certification of forecast skill, positive skill values, decay rates and the Lorenz limit. It implements the module claim that the number of timescales matches configuration dimension D = 5, aligning with the Recognition Science phi-ladder prediction for adjacent horizon skill ratios near 1/φ. No open scaffolding remains in this enumeration step.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.