forecastCost_zero_at_unit
The declaration shows that the forecast J-cost on the uncertainty growth ratio vanishes exactly at unit ratio. Climate predictability theorists would cite it to fix the zero baseline inside the J-cost formulation of forecast skill decay. The proof is a one-line wrapper that invokes the corresponding unit lemma from the core J-cost definition.
claimThe J-cost on the uncertainty growth ratio $r$ satisfies $J(1) = 0$, where $J(r) = (r-1)^2/(2r)$ is the recognition cost function.
background
In Recognition Science the J-cost is the function $J(r) = (r-1)^2/(2r)$, equivalently written as cosh(log r) - 1. The module Climate.PredictabilityFromJCost applies this cost to the uncertainty growth ratio $r = σ_forecast / σ_initial$ of a chaotic dynamical system. The predictability horizon is defined as the lead time at which $J(r)$ reaches the golden-section quantum $J(φ) ∈ (0.11, 0.13)$, marking the structural loss of deterministic forecast skill.
proof idea
The proof is a one-line wrapper that applies the lemma Jcost_unit0 from the Cost module (and its duplicate in JcostCore), which itself follows by direct simplification of the J-cost definition.
why it matters in Recognition Science
This result supplies the unit_zero field of the climatePredictabilityCert definition, which assembles the full certificate that forecast skill is structurally permitted while $J(r) < J(φ)$ and lost once $J(r) ≥ J(φ)$. It places climate predictability on the same footing as the universal RS quantum that gates plaque vulnerability, magnetic reconnection, and other transitions. The module thereby embeds the eight-tick octave and phi-ladder structures into operational forecast horizons.
scope and limits
- Does not compute the numerical value of the predictability threshold band.
- Does not model the growth rate of uncertainty in any concrete dynamical system.
- Does not incorporate model error or stochastic forcing beyond initial-condition ratio.
- Does not prove existence of a sharp horizon in current operational forecasts.
Lean usage
example : forecastCost 1 = 0 := forecastCost_zero_at_unitformal statement (Lean)
40theorem forecastCost_zero_at_unit : forecastCost 1 = 0 := Cost.Jcost_unit0
proof body
41