ClimateModelComponentsCert
plain-language theorem explainer
The structure asserts that the finite type of climate components has cardinality exactly five. Climate modelers working inside the Recognition Science framework cite it to lock the standard five-component GCM decomposition to configDim = 5. The declaration is a bare structure definition containing a single cardinality field and no proof obligations.
Claim. Let $C$ be the finite type whose elements are the five climate components atmosphere, ocean, land surface, cryosphere and biosphere/carbon cycle. The certificate structure is the record whose single field records that the cardinality of $C$ equals five.
background
The module introduces five canonical GCM components (atmosphere, ocean, land surface, cryosphere, biosphere/carbon cycle) that realize configDim $D=5$. The sibling inductive type enumerates exactly these five cases and derives the Fintype instance together with DecidableEq, Repr and BEq. The local theoretical setting is the B17 operational climate depth, which fixes the component count to match the dimensionality parameter of the Recognition Science climate model.
proof idea
The declaration is a structure definition whose sole field directly encodes the cardinality assertion. No lemmas or tactics are invoked; the definition itself supplies the certificate type.
why it matters
The structure supplies the type used by the downstream definition that populates the certificate via the count lemma. It fills the B17 climate depth step by confirming the five-component decomposition. In the wider framework the fixed count aligns configDim with standard GCM structure and supports any later derivations that depend on this cardinality.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.