horizonAtRung_pos
plain-language theorem explainer
Positivity of the forecast horizon at every natural-number rung on the phi-ladder is established. Climate predictability researchers cite the result when building certificates that compare ECMWF and GFS skill-decay horizons under the phi-ratio prediction. The term-mode proof unfolds the definition to a negative integer power of phi, invokes zpow_pos on Constants.phi_pos, and closes via linarith.
Claim. For every natural number $k$, the forecast horizon at rung $k$ (defined as $1 · ϕ^{-k}$) satisfies $0 < 1 · ϕ^{-k}$.
background
The module models operational forecast skill decay via the phi-ladder. The horizon at rung $k$ is referenceHorizon multiplied by phi to the power of negative $k$, where referenceHorizon is the dimensionless constant 1 calibrated to the ECMWF rung-0 level of roughly 10 days. The upstream Constants structure supplies phi_pos, and the module doc states that adjacent horizons ratio by exactly phi per rung, matching GFS at approximately 6-7 days.
proof idea
The proof is a one-line wrapper. It unfolds horizonAtRung and referenceHorizon to reduce the goal to $0 < phi^{(-(k:ℤ))}$, applies zpow_pos to Constants.phi_pos, and finishes with linarith.
why it matters
The lemma is invoked by horizon_adjacent_ratio, horizonAtRung_strictly_decreasing, and operationalForecastSkillCert. It supplies the required positivity anchor for the climate phi-ladder, consistent with the self-similar fixed point phi from the forcing chain. The module doc notes that a non-phi-rational distance between operational centers would falsify the structural prediction.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.