OperationalForecastSkillCert
OperationalForecastSkillCert bundles four properties of the forecast horizon function on the phi-ladder: positivity for every rung, exact one-step scaling by phi inverse, strict decrease, and the matching ratio identity. Climate modelers cite it to certify that ECMWF and GFS skill horizons obey the Recognition Science phi-ratio prediction. The structure is a direct packaging of four lemmas already proved for horizonAtRung.
claimA certificate that the forecast horizon function $h(k)$ at phi-ladder rung $k$ satisfies $h(k)>0$, $h(k+1)=h(k)cdotphi^{-1}$, $h(k+1)<h(k)$, and $h(k+1)/h(k)=phi^{-1}$ for all natural numbers $k$.
background
The module develops the Recognition Science claim that operational forecast skill horizons lie on the phi-ladder. The upstream definition sets horizonAtRung(k) := referenceHorizon * phi^(-k), where referenceHorizon is the ECMWF baseline (10 days) and negative rungs correspond to lower-resolution models that lose skill earlier. The module doc states that ECMWF (rung 0) and GFS (rung -1) horizons must therefore stand in the exact ratio phi^{-1}. This certificate structure collects the elementary analytic properties of that function into a single object that can be passed to downstream bridge theorems.
proof idea
The structure is defined by directly enumerating its four field axioms. No tactics or reductions occur inside the declaration itself. The downstream operationalForecastSkillCert instance populates the fields by applying the sibling lemmas horizonAtRung_pos, horizonAtRung_succ_ratio, horizonAtRung_strictly_decreasing, and horizon_adjacent_ratio.
why it matters in Recognition Science
The certificate supplies the formal interface for the operational-forecast-skill prediction inside the Recognition framework. It is consumed by operationalForecastSkillCert to produce a concrete instance that certifies the phi-ratio between ECMWF and GFS horizons. The construction sits inside the J-cost predictability analysis and realizes the self-similar fixed-point step (T6) of the forcing chain for the phi-ladder. It leaves open the empirical test against any third operational center whose horizon deviates from a phi-rational rung.
scope and limits
- Does not compute numerical horizon values for any specific model.
- Does not prove that referenceHorizon equals 10 days.
- Does not address the predictability cutoff theorems in the companion PredictabilityFromJCost module.
- Does not treat non-integer rungs or continuous resolution changes.
formal statement (Lean)
80structure OperationalForecastSkillCert where
81 horizon_pos : ∀ k, 0 < horizonAtRung k
82 one_step_ratio : ∀ k, horizonAtRung (k + 1) = horizonAtRung k * phi⁻¹
83 strictly_decreasing : ∀ k, horizonAtRung (k + 1) < horizonAtRung k
84 adjacent_ratio_eq_inv_phi :
85 ∀ k, horizonAtRung (k + 1) / horizonAtRung k = phi⁻¹
86
87/-- Operational-forecast-skill certificate. -/