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

WeatherPredictabilityCert

show as:
view Lean formalization →

The weather predictability certificate structure requires exactly five discrete prediction time ranges together with satisfaction of the canonical J-cost band conditions. Atmospheric modelers working in Recognition Science would cite it when mapping Lorenz unpredictability to J-dynamics decay. It is introduced as a bare structure definition that packages two fields with no lemmas or computational steps.

claimA weather predictability certificate consists of the assertion that the inductive type of five weather prediction intervals has cardinality five, together with an instance of the canonical J-cost certificate whose clauses include $J(1)=0$, reciprocity $J(x)=J(1/x)$, positivity at the golden ratio, the numerical band $0.11 < J(phi) < 0.13$, and positivity at $1/phi^2$.

background

The meteorology module models weather predictability via J-cost dynamics, where the ratio of actual to predicted states obeys the J functional equation and the cutoff occurs at the canonical J(phi) band. PredictionRange enumerates the five canonical intervals nowcast (0-2 h), short-range (2-24 h), medium (1-10 d), extended (10-30 d), and seasonal (30 d+), which the module identifies with configDim D = 5. The upstream CanonicalCert supplies the six-clause J-certificate reused across domains: matched zero at unity, reciprocity under inversion, positivity at phi, the explicit band 0.11 to 0.13, and recovery positivity at the inverse square.

proof idea

The declaration is a structure definition that directly declares the two fields cardinality condition on the five-range inductive type and reference to CanonicalCert. No lemmas are applied and no tactics are used; it functions as a record type with no proof obligations.

why it matters in Recognition Science

This structure supplies the type instantiated by the concrete certificate weatherPredictabilityCert, which populates the five-range count via predictionRangeCount and the skill threshold via the canonical J-band instance. It encodes the Recognition Science claim that weather skill decays inside the five-range partition according to J-cost, linking directly to J-uniqueness and the phi fixed point that set the predictability cutoff at roughly 14 days. It touches the open calibration of Lyapunov doubling time to the phi-ladder rung.

scope and limits

formal statement (Lean)

  29structure WeatherPredictabilityCert where
  30  five_ranges : Fintype.card PredictionRange = 5
  31  skill_threshold : CanonicalCert
  32

used by (1)

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.