pith. machine review for the scientific record. sign in
def definition def or abbrev high

IsWithinHorizon

show as:
view Lean formalization →

Forecast uncertainty ratio r lies inside the predictability horizon precisely when its J-cost is strictly less than the golden-section quantum J(φ). Climate modelers cite the definition to locate the sharp boundary between retained deterministic skill and structural loss of predictability. The definition is realized directly as the inequality between forecastCost r and PredictabilityThreshold.

claimA real number $r$ satisfies the within-horizon condition precisely when $J(r) < J(φ)$, where $J$ denotes the recognition cost function and $φ$ the golden ratio.

background

The module equates the climate predictability horizon to the lead time at which initial-condition uncertainty growth ratio r crosses the canonical golden-section quantum. Forecast skill is structurally permitted while J(r) stays below J(φ) and is lost once the threshold is met or exceeded. Upstream, forecastCost wraps Cost.Jcost r while PredictabilityThreshold fixes the value at Cost.Jcost φ, implementing the same band that gates plaque vulnerability, combustion ignition, and magnetic reconnection.

proof idea

The definition is a one-line wrapper that applies the strict inequality between forecastCost r and PredictabilityThreshold.

why it matters in Recognition Science

This definition supplies the positive half of the horizon partition used by ClimatePredictabilityCert and the exclusivity theorem horizon_states_exclusive. It realizes the module claim that deterministic forecast skill is permitted only for J(r) < J(φ), placing climate predictability on the same footing as the universal RS quantum band. No open questions are flagged in the supplied material.

scope and limits

formal statement (Lean)

  58def IsWithinHorizon (r : ℝ) : Prop := forecastCost r < PredictabilityThreshold

proof body

Definition body.

  59

used by (2)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (2)

Lean names referenced from this declaration's body.