module module moderate

`IndisputableMonolith.Climate.PredictabilityFromJCost`

The module defines forecastCost as the J-cost on the uncertainty growth ratio, plus horizon predicates and the ClimatePredictabilityCert. Climate modelers or Recognition Science users would cite it to bound predictability from the J-function. It assembles definitions and basic algebraic properties drawn from the imported Cost and Constants modules.

claimLet $r$ be the uncertainty growth ratio. Define $f(r) := J(r)$ as the forecast cost. The module introduces the threshold predicate, the mutually exclusive states IsPastHorizon and IsWithinHorizon, and the certificate ClimatePredictabilityCert together with its constructor.

background

The module belongs to the climate domain of Recognition Science. It imports the fundamental time quantum τ₀ = 1 tick from Constants and the J-cost machinery from Cost. Central definitions include forecastCost applied to the uncertainty growth ratio, with lemmas establishing zero at unit ratio, reciprocal symmetry, nonnegativity, and positivity away from unity. Horizon states are shown exclusive and a predictability threshold band is identified.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

The module supplies the J-cost forecast and certificate for climate predictability horizons. It extends the core J-uniqueness and phi fixed point to domain-specific forecasting, supporting the ClimatePredictabilityCert and the broader application of the forcing chain to uncertainty growth.

scope and limits

Does not simulate specific climate scenarios or integrate observational data.
Does not derive numerical predictability horizons beyond the abstract band.
Does not address multi-scale or external forcing corrections to the J-cost.
Does not prove uniqueness or completeness of the predictability certificate.

depends on (2)

Lean names referenced from this declaration's body.

IndisputableMonolith.Constants module_import
IndisputableMonolith.Cost module_import

declarations in this module (12)

def forecastCost L38
theorem forecastCost_zero_at_unit L40
theorem forecastCost_reciprocal_symm L42
theorem forecastCost_nonneg L45
theorem forecastCost_pos_off_unit L48
def PredictabilityThreshold L52
def IsPastHorizon L55
def IsWithinHorizon L58
theorem horizon_states_exclusive L60
theorem predictability_threshold_band L65
structure ClimatePredictabilityCert L81
def climatePredictabilityCert L92