forecastTimescaleCount
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.
claimLet $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 in Recognition Science
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.
scope and limits
- Does not derive the numerical skill percentages (99 percent, 90 percent, etc.) from the J-cost equation.
- Does not prove the adjacent-horizon skill ratio equals 1/φ.
- Does not establish the Lorenz limit of approximately 14 days.
- Does not relate the five timescales to the spatial dimension D = 3 of the core framework.
Lean usage
have h : Fintype.card ForecastTimescale = 5 := forecastTimescaleCountformal statement (Lean)
33theorem forecastTimescaleCount : Fintype.card ForecastTimescale = 5 := by decide
proof body
34