horizonAtRung
plain-language theorem explainer
horizonAtRung defines the forecast horizon at rung k on the phi-ladder as referenceHorizon scaled by phi to the power of minus k. Climate modelers comparing skill decay across ECMWF, GFS and lower-resolution centers would cite this explicit scaling. It is a direct definition that multiplies the unit reference by the inverse-phi factor at each integer rung.
Claim. The forecast horizon at rung $k$ is $h(k) = 1 · φ^{-k}$, where $φ$ is the golden ratio and the reference horizon at rung zero is normalized to 1.
background
The module sets operational forecast skill on the phi-ladder, with skill horizons decaying by successive factors of $φ^{-1}$ between resolution rungs. referenceHorizon supplies the baseline value 1 calibrated to the ECMWF IFS rung-0 horizon of roughly 10 days useful skill (ACC ≥ 0.6). The definition places rung $k$ at $φ^{-k}$, so rung 1 yields $φ^{-1} ≈ 0.618$ times the reference and rung 2 yields $φ^{-2} ≈ 0.382$ times the reference.
proof idea
Direct definition that unfolds referenceHorizon and applies the integer power $φ^{-k}$ with $k$ cast to ℤ.
why it matters
This definition supplies the explicit scaling used by OperationalForecastSkillCert and the downstream ratio theorems horizon_adjacent_ratio, horizonAtRung_succ_ratio, horizonAtRung_pos and horizonAtRung_strictly_decreasing. It encodes the Recognition Science structural prediction that adjacent forecast horizons ratio by exactly $φ^{-1}$, consistent with the self-similar fixed point phi from the forcing chain. The module links the ladder to empirical ECMWF/GFS data and the predictability cutoff in PredictabilityFromJCost.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.