forecastCost_nonneg
plain-language theorem explainer
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.
Claim. For 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
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.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.