forecastSkill
plain-language theorem explainer
Forecast skill at horizon k is defined as the reciprocal of phi to the power k. Climate modelers working in the Recognition Science framework cite this when establishing exponential decay of predictability on the phi-ladder. The definition is a direct one-line assignment that supplies the base expression for positivity and ratio theorems.
Claim. The forecast skill at integer horizon $k$ is defined by $s(k) := φ^{-k}$, where $φ$ denotes the golden-ratio fixed point of the Recognition Science J-cost equation.
background
The Climate Forecast Skill from J-Cost module models operational forecast accuracy as decaying on a phi-ladder, with adjacent horizons related by the factor $1/φ$. Five canonical timescales are fixed by configDim $D=5$, and the Lorenz predictability limit is placed near 15 days. The module documentation states that skill ratios approximate $1/φ$ and that the 14-day limit is consistent with $45 × 0.33$.
proof idea
This is a direct definition that assigns the value $(phi ^ k)⁻¹$ to forecastSkill k. No lemmas or tactics are invoked; the expression serves as the unfolding target for the downstream positivity and decay theorems.
why it matters
The definition supplies the explicit functional form required by the ClimateForecastCert structure, which certifies five timescales, positive skill values, the decay ratio $φ^{-1}$, and the Lorenz limit of 15 days. It implements the Recognition Science prediction of phi-ladder decay for climate horizons and closes the operational climate component of the J-cost framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.