climateModelComponentsCert
plain-language theorem explainer
This definition supplies a certificate that a climate model uses exactly five components by filling the ClimateModelComponentsCert structure with the equality Fintype.card ClimateComponent = 5. Researchers formalizing general circulation models would reference it to lock in the configDim D = 5 convention. It is assembled as a direct one-line assignment from the decided count theorem.
Claim. Let $C$ be the finite type of climate components. The structure ClimateModelComponentsCert requires that the cardinality $|C| = 5$. The definition climateModelComponentsCert is the witness that sets the five_components field to the theorem establishing $|C| = 5$.
background
The module sets five canonical GCM components (atmosphere, ocean, land surface, cryosphere, biosphere/carbon cycle) equal to configDim D = 5. ClimateModelComponentsCert is the structure whose single field is the proposition Fintype.card ClimateComponent = 5. The upstream theorem climateComponent_count proves this cardinality equality by decision procedure.
proof idea
One-line wrapper that directly supplies the climateComponent_count theorem as the witness for the five_components field of the certificate structure.
why it matters
This definition completes the operational climate depth B17 by certifying the five-component decomposition required for configDim D = 5. It stands as the Lean witness for the component count in climate modeling applications of the Recognition framework. No downstream uses or open questions are recorded.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.