inductive
definition
GeoengineeringApproach
show as:
view math explainer →
open explainer
Generate a durable explainer page for this declaration.
open lean source
IndisputableMonolith.Climate.GeoengineeringRiskFromJCost on GitHub at line 33.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
used by
formal source
30namespace IndisputableMonolith.Climate.GeoengineeringRiskFromJCost
31open Common.CanonicalJBand
32
33inductive GeoengineeringApproach where
34 | SAI | MCB | OIF | DAC | enhancedWeathering
35 deriving DecidableEq, Repr, BEq, Fintype
36
37theorem approachCount : Fintype.card GeoengineeringApproach = 5 := by decide
38
39structure GeoengineeringRiskCert where
40 five_approaches : Fintype.card GeoengineeringApproach = 5
41 risk_threshold : CanonicalCert
42
43noncomputable def geoengineeringRiskCert : GeoengineeringRiskCert where
44 five_approaches := approachCount
45 risk_threshold := cert
46
47end IndisputableMonolith.Climate.GeoengineeringRiskFromJCost