forecastCost_reciprocal_symm
plain-language theorem explainer
forecastCost_reciprocal_symm establishes that the J-cost on an uncertainty growth ratio r equals the J-cost on its reciprocal. Climate predictability researchers cite it when confirming symmetric treatment of forward and inverse uncertainty factors in chaotic forecasts. The proof is a direct one-line wrapper applying the Jcost_symm lemma from the Cost module to the forecastCost definition.
Claim. For every positive real number $r$, the forecast J-cost satisfies $J(r) = J(r^{-1})$, where $J$ denotes the recognition cost function applied to the uncertainty growth ratio $r = σ_{forecast}/σ_{initial}$.
background
The module Climate.PredictabilityFromJCost defines the predictability horizon as the lead time at which initial-condition uncertainty grows by a ratio $r$ such that the J-cost reaches the golden-section quantum $J(φ) ∈ (0.11, 0.13)$. forecastCost is the abbreviation forecastCost r := Cost.Jcost r, with Cost the RS-native quantity of type CostUnit. The upstream lemma Jcost_symm states that Jcost x = Jcost x^{-1} for x > 0, proved by unfolding the definition Jcost x = (x + x^{-1})/2 - 1, applying field_simp, and normalizing with ring.
proof idea
The declaration is a one-line wrapper that applies the lemma Jcost_symm from IndisputableMonolith.Cost (and its core variant) directly to the definition of forecastCost.
why it matters
This supplies the reciprocal_symm field required by the downstream climatePredictabilityCert, the assembled certificate that also includes non-negativity, threshold band, and exclusive horizon states. The symmetry aligns the climate application with the universal J-cost properties used across RS thresholds such as plaque vulnerability, magnetic reconnection, and the phi-ladder mass formula. It closes one structural requirement for the deterministic horizon prediction stated in the module documentation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.