GeoengineeringApproach
plain-language theorem explainer
The inductive type enumerates five canonical geoengineering methods as the discrete domain for Recognition Science climate risk models. Climate modelers assessing J-cost profiles against the safe band would cite this enumeration when counting options or certifying deployment thresholds. It is introduced directly as an inductive with deriving clauses that supply DecidableEq, Repr, BEq and Fintype.
Claim. Let $G$ be the finite set of geoengineering approaches. Then $G$ consists exactly of the five elements stratospheric aerosol injection, marine cloud brightening, ocean iron fertilisation, carbon dioxide removal and cirrus cloud thinning, equipped with decidable equality and finite cardinality.
background
Recognition Science evaluates geoengineering options on a J-cost ladder obtained from the functional equation J(xy) + J(x/y) = 2J(x)J(y) + 2J(x) + 2J(y), with J(x) = (x + x^{-1})/2 - 1. The module treats the five approaches as the concrete realisation of configDim = 5. Safe deployment is defined by the interval (0.11, 0.13) around the canonical J(φ) value on the perturbation ratio, where φ is the self-similar fixed point forced at T6.
proof idea
The declaration is a direct inductive definition of five constructors. The deriving clauses for DecidableEq, Repr, BEq and Fintype are supplied automatically by Lean; no separate proof body is required.
why it matters
This definition supplies the finite domain whose cardinality is asserted equal to 5 in the downstream theorems geoengineeringApproach_count and GeoengineeringCert. It thereby anchors the climate module to configDim = 5 and to the J(φ) safe band used in GeoengineeringRiskCert. The construction closes the discrete enumeration step required before any risk-profile or certification statements can be stated.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.