GeoengineeringRiskCert
plain-language theorem explainer
GeoengineeringRiskCert packages a structure requiring exactly five geoengineering approaches together with a canonical J-band certificate as the risk threshold. Climate modelers applying Recognition Science to intervention cascades would cite this when bounding flux-ratio perturbations. The declaration is a bare structure definition with no proof obligations or lemmas.
Claim. A geoengineering risk certificate consists of the statement that there are exactly five geoengineering approaches together with an instance of the canonical J-band certificate requiring $J(1)=0$, reciprocity under inversion, $J(phi)>0$, the interval $0.11 < J(phi) < 0.13$, and recovery positivity at $1/phi^2$.
background
The module treats geoengineering interventions as perturbations to the recognition ratio r with associated J-cost. It enumerates five canonical approaches via the inductive type whose constructors are stratospheric aerosol injection, marine cloud brightening, ocean iron fertilisation, direct air capture, and enhanced weathering. The risk threshold reuses CanonicalCert, whose six clauses encode the zero at unity, reciprocity, positivity at phi, the numerical band around J(phi), and recovery positivity.
proof idea
The declaration is a structure definition that directly bundles the cardinality field and the CanonicalCert instance. No lemmas are applied and no tactics are used.
why it matters
The structure is instantiated by geoengineeringRiskCert to supply concrete values for the five approaches and the threshold. It anchors climate risk assessment in the J-cost formalism and the phi band, supporting the claim that interventions must remain inside the recognition band to avoid cascade failure. It connects to T5 J-uniqueness and the phi fixed point.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.