CarbonRemovalCert
plain-language theorem explainer
CarbonRemovalCert is a structure asserting that the set of carbon removal pathways has cardinality exactly five. Climate modelers in the Recognition Science framework cite it to fix configDim D = 5 for the sector covering biological uptake through mineral sequestration. The declaration is a bare structure definition whose single field is later instantiated by a count lemma.
Claim. Let $P$ be the finite set of five canonical carbon-dioxide removal pathways (afforestation, soil carbon, biochar, direct air capture, enhanced weathering). Then CarbonRemovalCert is the structure whose sole field asserts $|P| = 5$.
background
The module models carbon removal with exactly five pathways to match the Recognition Science configDim parameter D = 5. CarbonRemovalPathway is the inductive type whose constructors are afforestation, soilCarbon, biochar, directAirCapture, and enhancedWeathering; it derives Fintype so that cardinality is computable. These five together cover biological uptake, soil storage, stable biomass, engineered capture, and mineral sequestration.
proof idea
The declaration is a structure definition containing no proof body, tactics, or lemmas. Its single field five_pathways is a Prop that stands open for later instantiation by the sibling count definition carbonRemovalPathway_count.
why it matters
The structure fixes the dimensionality of the climate submodule at five pathways, consistent with the E4/B17 climate depth and the configDim D = 5 convention. It is directly used by the concrete instance carbonRemovalCert, which supplies the cardinality value. No open questions or scaffolding are attached; the module reports zero axioms or sorrys.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.