climateComponent_count
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.
claimThe 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 in Recognition Science
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.
scope and limits
- Does not derive the count five from deeper Recognition Science forcing chain steps.
- Does not specify dynamical equations or interactions among the components.
- Does not incorporate physical constants such as G or alpha.
- Does not claim uniqueness of this five-component decomposition.
Lean usage
def climateModelComponentsCert : ClimateModelComponentsCert where five_components := climateComponent_countformal statement (Lean)
23theorem climateComponent_count : Fintype.card ClimateComponent = 5 := by decide
proof body
24