GeoengineeringApproach
plain-language theorem explainer
The inductive definition enumerates five canonical geoengineering interventions for Recognition Science climate modeling. Climate researchers cite it when classifying flux-ratio perturbations by their J-cost impact on the recognition cascade. The declaration is a direct inductive type with derived Fintype and decidable-equality instances that enable immediate cardinality proofs.
Claim. Let $A$ be the finite set of geoengineering approaches consisting of stratospheric aerosol injection (SAI), marine cloud brightening (MCB), ocean iron fertilisation (OIF), direct air capture (DAC), and enhanced weathering, equipped with decidable equality and finite-type structure.
background
Recognition Science treats geoengineering as a perturbation to the climate recognition cascade via the flux ratio $r$. The module states that an intervention is safe precisely when the induced J-cost on $r$ remains inside the canonical band around $J(φ)$; values below $1/φ$ push the ledger into deficit and raise termination-shock risk. Five approaches are fixed to match configDim $D=5$ and are listed explicitly in the module documentation.
proof idea
The declaration is a direct inductive definition that enumerates the five constructors and derives DecidableEq, Repr, BEq, and Fintype instances in one step.
why it matters
This enumeration is the source type for downstream results including approachCount (which proves cardinality 5) and GeoengineeringRiskCert (which pairs the count with CanonicalCert). It supplies the concrete list required by the module's risk-assessment framework that links J-cost bounds to the five interventions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.