weatherPredictabilityCert
plain-language theorem explainer
The definition assembles a certificate asserting exactly five canonical weather prediction ranges together with a skill threshold from the canonical J-band. Meteorologists modeling predictability horizons in the Recognition Science setting would cite it to link Lorenz instability to the J-cost dynamics and configuration dimension D equals 5. The construction is a direct record literal that substitutes the decidable cardinality theorem into the five_ranges field and assigns the skill threshold to the canonical certificate.
Claim. Let $W$ be the structure whose fields are five_ranges : Fintype.card$(P)=5$ for the finite type $P$ of prediction ranges, and skill_threshold : CanonicalCert. The weather predictability certificate is the instance of $W$ with five_ranges instantiated by the theorem establishing that cardinality equals five and skill_threshold set to the canonical certificate.
background
In the Recognition Science treatment of meteorology the J-cost functional equation governs the ratio of actual to predicted states. The module defines five prediction ranges corresponding to the configuration dimension D equals 5: nowcast (0-2 h), short (2-24 h), medium (1-10 d), extended (10-30 d), and seasonal (30 d+). The upstream result predictionRangeCount establishes by decision that the finite type of PredictionRange has cardinality exactly 5. The structure WeatherPredictabilityCert packages this cardinality together with a skill threshold drawn from the CanonicalCert.
proof idea
The definition is a one-line record constructor. It populates the five_ranges field by direct reference to the theorem predictionRangeCount. The skill_threshold field is assigned the canonical certificate value.
why it matters
This definition supplies the concrete certificate required to instantiate the meteorology application of the J-cost framework. It realizes the prediction of five ranges required by the configuration dimension in the unified forcing chain. No downstream uses are recorded yet, but it closes the scaffolding for weather predictability claims within the Recognition Science monolith. It touches the open question of deriving the precise Lyapunov time from the phi-ladder without external input.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.