CarbonRemovalPathway
plain-language theorem explainer
The inductive definition enumerates five canonical CO2 removal pathways to realize configDim D=5 in the climate module. Climate modelers cite it when establishing the discrete basis for pathway counting or verifying the finite set of mechanisms. It is introduced as a plain inductive type whose deriving clause supplies Fintype, Repr, and decidable equality with no further proof obligations.
Claim. Let $P$ be the finite set of carbon removal pathways whose elements are afforestation, soil-carbon sequestration, biochar production, direct-air capture, and enhanced weathering, equipped with decidable equality and the structure of a finite type.
background
The module sets configDim D=5 to index the five canonical carbon-dioxide-removal pathways. These comprise afforestation (biological uptake), soil carbon (soil storage), biochar (stable biomass), direct air capture (engineered capture), and enhanced weathering (mineral sequestration). The local setting states that the five together cover the principal classes of removal approaches, with the entire development free of axioms or sorrys.
proof idea
The declaration is an inductive definition with exactly five constructors followed by a deriving clause that installs DecidableEq, Repr, BEq, and Fintype. No tactic steps or lemmas are invoked; the finite-type instance is obtained automatically from the inductive structure.
why it matters
The definition supplies the carrier set whose cardinality is asserted equal to 5 in the downstream CarbonRemovalCert structure and the carbonRemovalPathway_count theorem. It realizes the configDim D=5 slot inside the E4/B17 climate depth, providing the discrete enumeration required for pathway counting. No open questions or scaffolding remain attached to this enumeration.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.