forecastCost_nonneg
Non-negativity of the J-cost on the uncertainty growth ratio is recorded for all positive ratios. Climate predictability researchers would cite it when certifying horizon thresholds inside the recognition framework. The proof is a direct one-line application of the general J-cost non-negativity lemma to the forecastCost definition.
claimFor every real $r > 0$, $0 ≤ J(r)$ where $J(r)$ denotes the J-cost of the forecast uncertainty ratio.
background
The PredictabilityFromJCost module defines forecastCost as the J-cost applied to the ratio $r$ of forecast to initial uncertainty. The J-cost is the function $J(x) = (x + x^{-1})/2 - 1$, known to be non-negative for $x > 0$ by the AM-GM inequality. The module sets the predictability horizon at the lead time where this cost reaches $J(φ)$, with $φ$ the golden ratio.
proof idea
The proof is a one-line wrapper applying the Jcost_nonneg lemma from the Cost module directly to the argument $r$ under the hypothesis $0 < r$.
why it matters in Recognition Science
It supplies the cost_nonneg field of the ClimatePredictabilityCert structure that assembles the full predictability-horizon certificate. This places climate forecasting inside the recognition framework alongside other phenomena gated by the same $J(φ)$ band. The module contrasts the sharp RS horizon with conventional soft skill cutoffs.
scope and limits
- Does not compute the numerical lead time of the horizon.
- Does not prove the result for $r ≤ 0$.
- Does not model the time evolution of the uncertainty ratio.
- Does not validate against observational climate data.
formal statement (Lean)
45theorem forecastCost_nonneg {r : ℝ} (hr : 0 < r) :
46 0 ≤ forecastCost r := Cost.Jcost_nonneg hr
proof body
47