climateComponent_count
plain-language theorem explainer
The theorem fixes the cardinality of the climate component type at exactly five, enumerating the standard general circulation model breakdown into atmosphere, ocean, land surface, cryosphere, and biosphere-carbon cycle. Climate modelers using formal verification would cite it to anchor the configDim parameter. The proof is a one-line wrapper that invokes the decide tactic on the derived Fintype instance.
Claim. The finite type of climate components, consisting of atmosphere, ocean, land surface, cryosphere, and biosphere-carbon cycle, has cardinality five: $|ClimateComponent| = 5$.
background
The module introduces an inductive type with five constructors that enumerate the canonical GCM components: atmosphere, ocean, landSurface, cryosphere, biosphereCarbon. These set the operational depth for climate modeling at configDim D = 5 under the B17 framework. The inductive definition automatically derives DecidableEq, Repr, BEq, and Fintype, supplying the finite cardinality used downstream.
proof idea
The proof is a one-line wrapper that applies the decide tactic. This tactic directly computes Fintype.card from the five constructors of the inductive type and confirms the equality holds.
why it matters
The result populates the five_components field of climateModelComponentsCert, certifying the component count for the climate model. It fixes a dimensional parameter in the Recognition Science climate layer, parallel to the spatial D = 3 and eight-tick octave landmarks, with no open questions or scaffolding remaining.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.