ClimateForecastCert
plain-language theorem explainer
The certification structure for climate forecast skill packages five forecast timescales, positive skill values, geometric decay by the inverse of phi, and the 15-day Lorenz limit into one record. Operational meteorologists would cite it to confirm that forecast skill follows the Recognition Science phi-ladder. The declaration is a plain structure definition that assembles the skill function and the five-element forecast timescale type.
Claim. The structure requires that the set of forecast timescales has cardinality 5, that the skill function $s(k)$ satisfies $0 < s(k)$ for every natural number $k$, that $s(k+1)/s(k) = phi^{-1}$, and that the Lorenz predictability limit equals 15 days.
background
The module models climate forecast skill as decaying on the phi-ladder with adjacent horizons related by the factor $1/phi$. ForecastTimescale is the inductive type with five constructors shortRange, medium, extended, monthly, and seasonal. The function forecastSkill k returns $phi^{-k}$. The constant lorenzLimitDays is fixed at 15 to match the gap-45/3 approximation of the two-week predictability barrier.
proof idea
The declaration is a structure definition. It directly encodes the four fields without invoking lemmas or tactics: the Fintype cardinality of the forecast timescale type, the positivity and ratio properties of the skill function, and the equality for the Lorenz limit.
why it matters
This structure certifies the B17 Climate Operational model. It is instantiated by the downstream climateForecastCert definition, which supplies the concrete values from the skill positivity, decay, and limit properties. The construction ties forecast skill decay to the phi-ladder and places the Lorenz limit at 15 days, consistent with the predicted skill ratios of approximately $1/phi$.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.