forecastCost
plain-language theorem explainer
forecastCost assigns the J-cost to the uncertainty growth ratio r, serving as the metric for when climate forecast skill is lost. Climate predictability researchers using Recognition Science would cite it to define the sharp horizon at J(φ). It is implemented as a direct alias to the Jcost function in the Cost module.
Claim. Let $J$ be the J-cost function on positive reals. The forecast cost on uncertainty growth ratio $r$ is defined by $forecastCost(r) := J(r)$.
background
The module derives the climate predictability horizon from the J-cost on the initial-condition uncertainty ratio $r := σ_forecast / σ_initial$. The J-cost satisfies the Recognition Composition Law $J(xy) + J(x/y) = 2J(x)J(y) + 2J(x) + 2J(y)$, vanishes at unity, and is nonnegative with symmetry under reciprocal. Upstream, Cost is the quantity type Quantity CostUnit in RS-native units, supplying the Jcost function with the listed algebraic properties.
proof idea
The definition is a one-line wrapper that applies Cost.Jcost to the input ratio r.
why it matters
This definition supplies the cost measure used in ClimatePredictabilityCert to certify the predictability horizon and in the predicates IsPastHorizon and IsWithinHorizon. It connects climate forecasting to the universal RS quantum $J(φ) ∈ (0.11, 0.13)$, placing it alongside plaque vulnerability, magnetic reconnection, and other gated phenomena. It fills the step from T5 J-uniqueness to a concrete predictability application.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.