row_sin2_thetaW_codata_bracket

formal source

  31
  32def row_sin2_thetaW_codata : ℝ := WeinbergAngle.sin2ThetaW_observed
  33
  34theorem row_sin2_thetaW_codata_bracket :
  35    (0.22 : ℝ) < row_sin2_thetaW_codata ∧ row_sin2_thetaW_codata < (0.23 : ℝ) := by
  36  simpa [row_sin2_thetaW_codata] using WeinbergAngle.sin2_theta_bounds
  37
  38theorem row_sin2_thetaW_RS_bracket :
  39    0.228 < sin2ThetaW_RS ∧ sin2ThetaW_RS < 0.232 := sin2ThetaW_RS_approx
  40
  41theorem row_best_prediction_match :
  42    |WeinbergAngle.bestPrediction - row_sin2_thetaW_codata| < 0.01 :=
  43  WeinbergAngle.best_prediction_close_to_observed
  44
  45structure WeinbergAngleScoreCardCert where
  46  codata_in_ref_band :
  47    (0.22 : ℝ) < row_sin2_thetaW_codata ∧ row_sin2_thetaW_codata < (0.23 : ℝ)
  48  rs_bracket : 0.228 < sin2ThetaW_RS ∧ sin2ThetaW_RS < 0.232
  49  one_cent_match : |WeinbergAngle.bestPrediction - row_sin2_thetaW_codata| < 0.01
  50
  51theorem weinbergAngleScoreCardCert_holds : Nonempty WeinbergAngleScoreCardCert :=
  52  ⟨{ codata_in_ref_band := row_sin2_thetaW_codata_bracket
  53     rs_bracket := row_sin2_thetaW_RS_bracket
  54     one_cent_match := row_best_prediction_match }⟩
  55
  56end
  57
  58end IndisputableMonolith.Physics.WeinbergAngleScoreCard