forecastCost_pos_off_unit
The theorem establishes that forecast cost on an uncertainty growth ratio r remains strictly positive for every positive r distinct from one. Climate modelers would cite it to confirm that predictability horizons stay well-defined away from the unit ratio. The proof is a direct one-line application of the general positivity lemma for the J-cost function.
claimLet $r$ be a positive real number with $r ≠ 1$. Then the forecast cost on the uncertainty growth ratio satisfies $0 <$ forecastCost$(r)$, where forecastCost denotes the J-cost applied to the ratio of forecast to initial uncertainty.
background
The module treats climate predictability as the lead time at which initial-condition uncertainty grows by a factor $r$ that drives the J-cost to the canonical threshold $J(φ)$. The forecast cost is introduced by the sibling definition forecastCost $r$ := Jcost $r$, with Jcost the recognition cost obeying the composition law $J(xy) + J(x/y) = 2J(x)J(y) + 2J(x) + 2J(y)$ and the positivity property that $J(x) > 0$ whenever $x > 0$ and $x ≠ 1$ (quoted from the upstream lemma Jcost_pos_of_ne_one). This local setting inherits the Recognition Science forcing chain in which $J(φ)$ marks the universal quantum separating permitted and lost predictability across multiple physical domains.
proof idea
The proof is a one-line wrapper that applies the lemma Jcost_pos_of_ne_one directly to the definition of forecastCost, substituting the supplied hypotheses $0 < r$ and $r ≠ 1$.
why it matters in Recognition Science
The result underwrites the structural claim that deterministic forecast skill is permitted while $J(r) < J(φ)$ and lost once $J(r) ≥ J(φ)$, placing climate predictability on the same footing as plaque vulnerability, magnetic reconnection and the other RS-gated transitions listed in the module. It supplies the positivity ingredient required by the sibling ClimatePredictabilityCert construction and the predictability_threshold_band predicate. No open scaffolding remains in this declaration.
scope and limits
- Does not compute a numerical horizon length in physical time units.
- Does not incorporate model error or stochastic forcing beyond the initial-condition ratio.
- Does not prove existence of a horizon for any concrete dynamical system.
- Does not address the precise location of $J(φ)$ inside the interval (0.11, 0.13).
formal statement (Lean)
48theorem forecastCost_pos_off_unit {r : ℝ} (hr : 0 < r) (hne : r ≠ 1) :
49 0 < forecastCost r := Cost.Jcost_pos_of_ne_one r hr hne
proof body
Term-mode proof.
50
51/-- Predictability-horizon threshold = canonical golden-section quantum. -/