IsWithinHorizon
plain-language theorem explainer
Forecast uncertainty ratio r lies inside the predictability horizon precisely when its J-cost is strictly less than the golden-section quantum J(φ). Climate modelers cite the definition to locate the sharp boundary between retained deterministic skill and structural loss of predictability. The definition is realized directly as the inequality between forecastCost r and PredictabilityThreshold.
Claim. A real number $r$ satisfies the within-horizon condition precisely when $J(r) < J(φ)$, where $J$ denotes the recognition cost function and $φ$ the golden ratio.
background
The module equates the climate predictability horizon to the lead time at which initial-condition uncertainty growth ratio r crosses the canonical golden-section quantum. Forecast skill is structurally permitted while J(r) stays below J(φ) and is lost once the threshold is met or exceeded. Upstream, forecastCost wraps Cost.Jcost r while PredictabilityThreshold fixes the value at Cost.Jcost φ, implementing the same band that gates plaque vulnerability, combustion ignition, and magnetic reconnection.
proof idea
The definition is a one-line wrapper that applies the strict inequality between forecastCost r and PredictabilityThreshold.
why it matters
This definition supplies the positive half of the horizon partition used by ClimatePredictabilityCert and the exclusivity theorem horizon_states_exclusive. It realizes the module claim that deterministic forecast skill is permitted only for J(r) < J(φ), placing climate predictability on the same footing as the universal RS quantum band. No open questions are flagged in the supplied material.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.