IsPastHorizon
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.
claimA 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 in Recognition Science
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).
scope and limits
- Does not compute numerical lead times for any specific dynamical model.
- Does not derive the numerical value of J(φ) from climate data.
- Does not extend the predicate to ensemble or stochastic forecasts.
formal statement (Lean)
55def IsPastHorizon (r : ℝ) : Prop := PredictabilityThreshold ≤ forecastCost r
proof body
Definition body.
56
57/-- Forecast is within the horizon iff its J-cost is strictly below. -/