  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
  55  band_inhabited := safeBand_contains_phi_point
  56
  57end IndisputableMonolith.Climate.GeoengineeringApproachesFromConfigDim

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.