ClimateComponent
plain-language theorem explainer
The declaration enumerates an inductive type with five constructors representing the standard components of a general circulation model. Climate modelers working in Recognition Science would cite it to fix configDim at five for B17 operational depth. The definition proceeds by direct inductive construction with automatic derivation of Fintype and equality instances.
Claim. Let $C$ be the finite set whose elements are atmosphere, ocean, land surface, cryosphere, and biosphere/carbon cycle.
background
The module supplies the component enumeration for B17 operational climate depth in Recognition Science. Five canonical GCM components are fixed to match configDim D = 5: atmosphere, ocean, land surface, cryosphere, biosphere / carbon cycle. No upstream lemmas are required; the declaration is a foundational inductive type.
proof idea
The declaration is a direct inductive definition that lists the five constructors and derives DecidableEq, Repr, BEq, and Fintype by the deriving clause.
why it matters
The type is consumed by the theorem climateComponent_count establishing Fintype.card = 5 and by the structure ClimateModelComponentsCert. It implements the B17 step that sets configDim to five, anchoring the climate layer of the Recognition framework to the same dimensional parameter used elsewhere for spatial and forcing structure.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.