ClimateComponent
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.
claimLet $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 in Recognition Science
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.
scope and limits
- Does not encode fluxes or interactions among the five components.
- Does not introduce differential equations or time-stepping.
- Does not specify numerical grids or discretization.
- Does not incorporate external forcing or boundary data.
formal statement (Lean)
15inductive ClimateComponent where
16 | atmosphere
17 | ocean
18 | landSurface
19 | cryosphere
20 | biosphereCarbon
21 deriving DecidableEq, Repr, BEq, Fintype
22