operationalForecastSkillCert
plain-language theorem explainer
Definition operationalForecastSkillCert assembles the certificate asserting that skill horizons on the phi-ladder are positive, decrease strictly by factor phi inverse at each rung, and satisfy adjacent ratios exactly equal to phi inverse. Climate predictability researchers comparing ECMWF and GFS skill decay would cite it to formalize the recognition-Lyapunov-time prediction. The construction is a direct structure literal that populates the four fields from the module's positivity, successor-ratio, decrease, and adjacent-ratio theorems.
Claim. Let $h(k)$ denote the forecast skill horizon at rung $k$. The certificate asserts that $h(k) > 0$ for all natural $k$, $h(k+1) = h(k) / phi$, $h(k+1) < h(k)$, and $h(k+1)/h(k) = 1/phi$ for all $k$.
background
The module models operational forecast skill decay via Lyapunov time on the phi-ladder. HorizonAtRung is defined as referenceHorizon scaled by phi to the power of minus the rung index, where referenceHorizon supplies the base value at rung zero. This encodes the structural prediction that skill horizons between operational centers stand in exact powers of phi, consistent with the Recognition Composition Law and the self-similar fixed point of phi.
proof idea
The definition is a direct structure constructor. It assigns horizon_pos to the positivity theorem horizonAtRung_pos, one_step_ratio to the successor ratio theorem horizonAtRung_succ_ratio, strictly_decreasing to the decrease theorem horizonAtRung_strictly_decreasing, and adjacent_ratio_eq_inv_phi to the ratio theorem horizon_adjacent_ratio. No additional tactics or reductions are applied.
why it matters
This definition supplies the top-level certificate for the climate module, realizing the phi-ratio prediction between centers such as ECMWF at rung zero and GFS at rung minus one. It compounds with PredictabilityFromJCost and rests on the phi fixed-point property from the forcing chain. The result supports the recognition prediction that adjacent forecast-skill horizons ratio by exactly phi per integer rung of model resolution.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.