gauge_sum_bounds

formal source

  55  unfold gauge_sum_prediction cube_edges
  56  simp [D]
  57
  58theorem gauge_sum_bounds :
  59    (36 : ℝ) < gauge_sum_prediction ∧ gauge_sum_prediction < (48 : ℝ) := by
  60  rw [gauge_sum_value]
  61  constructor <;> nlinarith [Real.pi_gt_three, Real.pi_lt_four]
  62
  63/-! ## Certificate -/
  64
  65structure StrongCouplingCert where
  66  positive : 0 < alpha_s_prediction
  67  gauge_structure : gauge_sum_prediction = 12 * Real.pi
  68  gauge_bounded : (36 : ℝ) < gauge_sum_prediction ∧ gauge_sum_prediction < 48
  69
  70theorem strong_coupling_cert_exists : Nonempty StrongCouplingCert :=
  71  ⟨{ positive := alpha_s_positive
  72     gauge_structure := gauge_sum_value
  73     gauge_bounded := gauge_sum_bounds }⟩
  74
  75end
  76
  77end IndisputableMonolith.Constants.StrongCoupling