predictionRangeCount
plain-language theorem explainer
The theorem fixes the cardinality of the canonical weather prediction ranges at five. Meteorologists applying J-cost dynamics to Lorenz-style predictability would cite this to set the dimension of the tiered forecast space. The proof is a one-line decide tactic that counts the five constructors of the inductive PredictionRange type.
Claim. The finite set of weather prediction time ranges has cardinality five, where the ranges are nowcast (0-2 h), short-range (2-24 h), medium-range (1-10 d), extended (10-30 d), and seasonal (30 d+).
background
The Meteorology module models weather predictability via J-cost dynamics, with the ratio of actual to predicted state governed by the canonical J(phi) band and a predictability cutoff at that band. PredictionRange is the inductive type whose five constructors enumerate the distinct forecast horizons; it derives DecidableEq, Repr, BEq, and Fintype so that cardinality is computable. The module documentation states that this enumeration equals configDim D = 5 and that skill scores decay as phi^(-t/T_c) with T_c approximately 14 days.
proof idea
The proof is a one-line wrapper that applies the decide tactic directly to the equality Fintype.card PredictionRange = 5. Because PredictionRange is an inductive type with exactly five constructors and already derives a Fintype instance, decide computes the cardinality by enumeration without invoking further lemmas.
why it matters
This cardinality supplies the five_ranges field inside the weatherPredictabilityCert definition, anchoring the meteorology model to five discrete predictability windows. It realizes the module claim that configDim D = 5 for weather ranges, consistent with the Recognition Science forcing chain in which discrete dimensions arise from J-uniqueness and self-similarity. The result precedes derivation of skill thresholds and the phi-powered decay law.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.