climatePredictabilityCert
plain-language theorem explainer
The climate predictability certificate assembles the J-cost properties of forecast uncertainty ratios into a single structure. Climate modelers cite it to mark the sharp transition from deterministic skill to loss once the initial-condition ratio crosses the golden-section band. The definition is a record constructor that directly assigns five upstream theorems to the structure fields.
Claim. A climate predictability certificate consists of the properties that forecast cost vanishes at unit ratio ($forecastCost(1)=0$), is symmetric under reciprocal ratios ($forecastCost(r)=forecastCost(r^{-1})$ for $r>0$), is nonnegative for positive ratios ($forecastCost(r)≥0$ for $r>0$), the predictability threshold lies in $(0.11,0.13)$, and within-horizon and past-horizon states are mutually exclusive.
background
The module derives climate forecast horizons from the J-cost function applied to the ratio of forecast to initial uncertainty. The J-cost is the recognition cost $J(r)=(r+1/r)/2-1$, which vanishes at $r=1$ and is symmetric under inversion. The predictability threshold is defined to lie in the band $J(φ)∈(0.11,0.13)$, where $φ$ is the golden ratio, marking the point at which initial-condition uncertainty growth renders deterministic forecasts structurally invalid.
proof idea
The definition constructs the ClimatePredictabilityCert record by assigning the unit-zero property from forecastCost_zero_at_unit, the reciprocal symmetry from forecastCost_reciprocal_symm, nonnegativity from forecastCost_nonneg, the threshold band from predictability_threshold_band, and state exclusivity from horizon_states_exclusive.
why it matters
This certificate supplies the structural prediction that deterministic skill persists while J(r)<J(φ) and is lost thereafter. It embeds climate predictability into the universal recognition band that also governs plaque vulnerability, magnetic reconnection, and other phase transitions listed in the module documentation. No downstream uses are recorded yet; the declaration closes the local axiomatization of the predictability horizon.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.