pith. machine review for the scientific record. sign in
module module high

IndisputableMonolith.Climate.OperationalForecastSkillFromJCost

show as:
view Lean formalization →

The module supplies definitions for reference forecast horizons in RS-native units calibrated to ECMWF rung 0 together with scaling lemmas and an operational forecast skill certificate derived from J-cost. Climate modelers and Recognition Science users would cite these objects when mapping rung-based accuracy to practical forecast horizons. The module consists of definitions and basic ratio lemmas with no complex proofs.

claimLet $h_0 = 1$ be the reference forecast horizon (dimensionless, RS-native, calibrated at ECMWF rung 0). For rung $r$ the horizon $h(r)$ satisfies $h(r) > 0$, the successor ratio $h(r+1)/h(r)$ is constant, and $h(r)$ is strictly decreasing. OperationalForecastSkillCert is the structure that certifies forecast skill from the J-cost.

background

The module sits in the climate domain and imports the RS time quantum from Constants, where the fundamental tick satisfies $τ_0 = 1$. It introduces referenceHorizon as the baseline horizon fixed at the dimensionless value 1 and calibrated to ECMWF rung 0. Subsequent definitions such as horizonAtRung supply the rung-dependent scaling on the phi-ladder, together with positivity, ratio, and monotonicity properties that prepare the ground for skill certification.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

The module supplies the core horizon objects and skill certificate that connect J-cost to operational climate forecasting. It feeds the Recognition Science framework at the point where rung scaling meets practical forecast accuracy, supporting later applications that link the phi-ladder to measurable skill metrics.

scope and limits

depends on (1)

Lean names referenced from this declaration's body.

declarations in this module (8)