forecastCost_pos_off_unit
plain-language theorem explainer
The theorem asserts that the J-cost on an uncertainty growth ratio is strictly positive for any positive ratio not equal to one. Climate modelers would cite it when bounding predictability horizons away from the degenerate no-growth case. The proof is a direct specialization of the general positivity lemma for the J-cost function.
Claim. Let $J(r)$ be the J-cost on the uncertainty growth ratio $r$. Then $J(r) > 0$ for all real $r > 0$ with $r ≠ 1$.
background
The module treats the climate predictability horizon as the lead time at which the J-cost on the initial-condition uncertainty ratio reaches the golden-section quantum. The forecast cost function is defined by applying the J-cost to the uncertainty growth ratio $r$. The J-cost satisfies $J(x) > 0$ whenever $x > 0$ and $x ≠ 1$, as shown by rewriting it as a square divided by a positive term once $x ≠ 0$. The upstream lemma Jcost_pos_of_ne_one supplies this positivity directly. The local setting states that deterministic forecast skill is permitted while $J(r) < J(φ)$ and lost once $J(r) ≥ J(φ)$, producing a sharp horizon rather than a soft cutoff.
proof idea
The proof is a one-line term that applies the lemma Jcost_pos_of_ne_one from the Cost module to the supplied arguments $r$, $hr$, and $hne$ after identifying the forecast cost with the underlying J-cost.
why it matters
This result supports the structural claim of a sharp predictability horizon by ensuring the cost measure is positive away from the unit ratio. It aligns climate predictability with the Recognition Science framework in which the same J-cost band gates plaque vulnerability, magnetic reconnection, and other thresholds. The module doc-comment places forecast skill alongside the universal RS quantum $J(φ) ∈ (0.11, 0.13)$. It fills a basic positivity step in the climate predictability development without touching open questions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.