WeatherPhenomenon
plain-language theorem explainer
Recognition Science equates the number of canonical weather phenomena to the configuration dimension D in its derivation of atmospheric equilibrium. This inductive definition enumerates the five cases high-pressure systems, low-pressure systems, fronts, jet streams, and ENSO. Atmospheric physicists working from the J-cost balance would cite the resulting cardinality when checking the C/E4 climate model. The declaration is a direct inductive type that derives Fintype for immediate use in automated counting.
Claim. Let $W$ be the inductive type whose constructors are high-pressure systems, low-pressure systems, atmospheric fronts, jet streams, and the El Niño-Southern Oscillation. Then $|W|=5$.
background
In Recognition Science, atmospheric stability is expressed by the J-cost function: positive J signals convective instability while J=0 marks equilibrium. The module identifies five canonical layers and five weather phenomena with the configuration dimension D. The supplied inductive definition supplies exactly those five phenomena so that downstream cardinality statements can be formed directly from Fintype.
proof idea
The declaration is a plain inductive definition with five constructors. It derives DecidableEq, Repr, BEq, and Fintype in a single line, enabling the decide tactic to compute the cardinality in the sibling theorem weatherPhenomenonCount.
why it matters
This definition supplies the five phenomena required by the AtmosphericPhysicsCert structure, which also asserts five layers and the equilibrium condition Jcost 1 = 0. It completes the enumeration step of the C/E4 climate model in which the number of phenomena equals configDim D. The parent theorem weatherPhenomenonCount then records the concrete equality Fintype.card WeatherPhenomenon = 5.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.