climateForecastCert
plain-language theorem explainer
climateForecastCert supplies a concrete record for the climate forecast certificate in the Recognition Science climate module. It assembles the five-timescale count, strict positivity of skill, geometric decay by the reciprocal of phi, and the fifteen-day Lorenz limit. The construction is a direct record literal that references four sibling theorems in the same file.
Claim. A climate forecast certificate asserting five forecast timescales, positivity of the skill function for every natural-number index, the ratio of successive skill values equal to the reciprocal of the golden ratio, and the Lorenz predictability limit fixed at fifteen days.
background
The module treats operational climate forecast skill as decaying on a phi-ladder derived from the J-cost function. Five canonical horizons (short-range through seasonal) are required to match configDim D = 5, with adjacent skill ratios fixed at phi inverse and the predictability horizon at fifteen days. The structure ClimateForecastCert packages exactly these four properties as a single record.
proof idea
The definition builds the record by direct field assignment. It sets the timescale count to the decide tactic result, positivity to the inverse-power positivity lemma, the decay ratio to the field-simplification proof of the geometric step, and the Lorenz limit to reflexivity.
why it matters
This definition completes the B17 Climate Operational certificate. It supplies the single concrete instance that any downstream climate model can cite to inherit the phi-ladder decay law and the five-timescale structure. It directly encodes the Recognition Science claim that forecast skill ratios equal phi inverse and that the Lorenz limit sits at gap-45/3 days.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.