PredictionRange
plain-language theorem explainer
PredictionRange enumerates the five standard meteorological forecast horizons that map onto the canonical J(phi) band in Recognition Science. Meteorologists and RS modelers cite the enumeration when converting the Lorenz two-week predictability limit into a discrete configDim D = 5. The declaration is a plain inductive type whose deriving clause supplies the Fintype instance used by downstream cardinality and certification results.
Claim. Let $P$ be the finite set whose elements are the five weather prediction intervals: nowcast (0-2 h), short-range (2-24 h), medium-range (1-10 d), extended (10-30 d), and seasonal (>30 d). Then $|P|=5$ and $P$ carries a decidable equality and Fintype structure.
background
The module treats weather predictability through the ratio $r$ = (actual state) / (predicted state), which obeys J-cost dynamics whose cutoff lies inside the canonical J(phi) band. Five discrete ranges realize configDim D = 5, with the skill score predicted to decay as phi^(-t/T_c) where T_c approximates the 14-day Lyapunov doubling time. The module imports CanonicalJBand to supply the skill-threshold certificate that will later reference this enumeration.
proof idea
The declaration is an inductive definition that introduces exactly five constructors and derives DecidableEq, Repr, BEq, and Fintype in a single deriving clause; no explicit proof body is required.
why it matters
PredictionRange supplies the five_ranges field inside WeatherPredictabilityCert and the target of the cardinality theorem predictionRangeCount. It directly encodes the RS claim that meteorological predictability is governed by the same J-cost and phi-ladder structure that fixes D = 3 in the spatial case and the eight-tick octave, thereby linking the Lorenz butterfly cutoff to the Recognition Composition Law.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.