IsPastHorizon
plain-language theorem explainer
IsPastHorizon marks a forecast as past the predictability horizon when the J-cost on its uncertainty growth ratio r meets or exceeds the fixed threshold J(φ). Climate modelers cite the predicate to locate the structural cutoff of deterministic skill. The definition is a direct comparison of the golden-section constant to the forecastCost function.
Claim. A forecast with uncertainty growth ratio $r$ lies past the predictability horizon precisely when $J(r) ≥ J(φ)$, where $J$ is the recognition cost function and $φ$ the golden ratio.
background
The module treats climate predictability as the lead time at which initial-condition uncertainty grows by ratio $r := σ_forecast / σ_initial$ until the J-cost crosses the canonical threshold. forecastCost r is defined as the J-cost of that ratio; PredictabilityThreshold is defined as the J-cost of φ. Both rest on the upstream cost functions from MultiplicativeRecognizerL4 and ObserverForcing, which derive non-negative J-cost from recognition events on positive ratios.
proof idea
One-line definition that equates IsPastHorizon r to the inequality PredictabilityThreshold ≤ forecastCost r.
why it matters
The predicate supplies the right-hand side of the mutual-exclusion theorem horizon_states_exclusive and the threshold_band field inside ClimatePredictabilityCert. It encodes the module claim that deterministic skill is lost once J(r) ≥ J(φ), aligning climate forecasts with the same recognition threshold that gates plaque vulnerability, magnetic reconnection, and the other phenomena listed in the module doc. The relevant framework landmark is the golden-section quantum J(φ) ∈ (0.11, 0.13).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.