horizonAtRung_strictly_decreasing
plain-language theorem explainer
The theorem proves that forecast horizons on the phi-ladder decrease strictly with each integer increase in rung index. Climate researchers comparing skill decay across operational centers such as ECMWF and GFS would cite it to ground the phi-ratio prediction. The proof rewrites the successor via the ratio lemma, invokes positivity of the current horizon, and multiplies by the fact that phi inverse is less than one.
Claim. For every natural number $k$, let $h(k)$ be the forecast horizon at rung $k$, given by $h(k) = H_0 phi^{-k}$ where $H_0$ is the reference horizon. Then $h(k+1) < h(k)$.
background
The module models operational forecast skill horizons via the phi-ladder, with the explicit prediction that adjacent centers differ by exactly the golden ratio per rung of resolution. The horizon function is defined as referenceHorizon times phi to the power of negative k. The successor ratio theorem states that the horizon at rung k+1 equals the horizon at k multiplied by phi inverse. The positivity theorem confirms every such horizon is positive. The module doc frames this as a structural test: ECMWF at rung 0 gives 10 days while GFS at rung -1 gives 10/phi, matching observed 6-7 day skill.
proof idea
The proof applies the successor ratio theorem to rewrite the left-hand side as the current horizon times phi inverse. It invokes the positivity theorem to obtain a positive multiplier, then uses the constants lemma phi greater than 1.5 together with the inverse-less-than-one fact to produce the strict inequality via left multiplication.
why it matters
This result supplies the strictly decreasing field required by the operationalForecastSkillCert definition, which bundles positivity, one-step ratio, strict decrease, and adjacent ratio into the certificate. It completes the ordering component of the phi-ladder forecast model, consistent with the self-similar fixed point phi from the recognition chain. No open scaffolding remains in this declaration.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.