GeoengineeringApproach

formal source

  21namespace IndisputableMonolith.Climate.GeoengineeringApproachesFromConfigDim
  22open Constants
  23
  24inductive GeoengineeringApproach where
  25  | stratosphericAerosol
  26  | marineCloudBrightening
  27  | oceanIronFertilisation
  28  | carbonDioxideRemoval
  29  | cirrusCloudThinning
  30  deriving DecidableEq, Repr, BEq, Fintype
  31
  32theorem geoengineeringApproach_count :
  33    Fintype.card GeoengineeringApproach = 5 := by decide
  34
  35/-- Safe-deployment ratio band matches canonical J(φ) band. -/
  36noncomputable def safeBandLower : ℝ := 0.11
  37noncomputable def safeBandUpper : ℝ := 0.13
  38
  39theorem safeBand_nondegenerate : safeBandLower < safeBandUpper := by
  40  unfold safeBandLower safeBandUpper; norm_num
  41
  42theorem safeBand_contains_phi_point :
  43    safeBandLower < 0.118 ∧ 0.118 < safeBandUpper := by
  44  unfold safeBandLower safeBandUpper
  45  refine ⟨?_, ?_⟩ <;> norm_num
  46
  47structure GeoengineeringCert where
  48  five_approaches : Fintype.card GeoengineeringApproach = 5
  49  band_well_defined : safeBandLower < safeBandUpper
  50  band_inhabited : safeBandLower < 0.118 ∧ 0.118 < safeBandUpper
  51
  52noncomputable def geoengineeringCert : GeoengineeringCert where
  53  five_approaches := geoengineeringApproach_count
  54  band_well_defined := safeBand_nondegenerate