CKMElementScoreCardCert

formal source

  43
  44theorem row_vub_eq_leakage : V_ub_pred = fine_structure_leakage := vub_derived
  45
  46structure CKMElementScoreCardCert where
  47  vus : abs (V_us_pred - V_us_exp) < V_us_err
  48  vcb : abs (V_cb_pred - V_cb_exp) < V_cb_err
  49  vub : abs (V_ub_pred - V_ub_exp) < V_ub_err
  50  vus_geo : V_us_pred = torsion_overlap - cabibbo_radiative_correction
  51  vcb_geo : V_cb_pred = edge_dual_ratio
  52  vub_geo : V_ub_pred = fine_structure_leakage
  53
  54theorem ckmElementScoreCardCert_holds : Nonempty CKMElementScoreCardCert :=
  55  ⟨{ vus := row_V_us
  56     vcb := row_V_cb
  57     vub := row_V_ub
  58     vus_geo := row_vus_eq_geometry
  59     vcb_geo := row_vcb_eq_geometry
  60     vub_geo := row_vub_eq_leakage }⟩
  61
  62end
  63
  64end IndisputableMonolith.Physics.CKMElementScoreCard