ClimateModelComponentsCert
The structure certifies that the climate model operates with exactly five components drawn from the enumerated type of atmosphere, ocean, land surface, cryosphere, and biosphere. Climate modelers working inside the Recognition Science framework cite it to lock configDim at 5 for general circulation simulations. The declaration is a bare structure definition with no proof obligations or lemmas.
claimLet $C$ be the finite type whose elements are atmosphere, ocean, land surface, cryosphere, and biosphere. The structure asserts that the cardinality of $C$ equals 5.
background
The module defines an inductive type ClimateComponent whose five constructors are atmosphere, ocean, landSurface, cryosphere, and biosphereCarbon. This enumeration is presented as the canonical set of general circulation model components and is tied directly to the configDim parameter fixed at 5. The module imports Mathlib for Fintype and IndisputableMonolith.Constants; its opening documentation states that the construction carries zero sorry or axiom.
proof idea
The declaration is a structure definition whose single field records the equality Fintype.card ClimateComponent = 5. No tactics or upstream lemmas are invoked; the field is simply part of the structure signature.
why it matters in Recognition Science
The structure is instantiated by the downstream definition climateModelComponentsCert, which supplies a concrete value for use in larger climate constructions. It supplies the B17 operational climate depth requirement by fixing the component count at five, consistent with the Recognition Science setting of configDim D = 5. No open questions or scaffolding are addressed.
scope and limits
- Does not encode the governing equations for any component.
- Does not derive the integer 5 from Recognition Science forcing steps.
- Does not contain simulation code or time-stepping logic.
formal statement (Lean)
25structure ClimateModelComponentsCert where
26 five_components : Fintype.card ClimateComponent = 5
27