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