row_V_us

formal source

  30
  31noncomputable section
  32
  33theorem row_V_us : abs (V_us_pred - V_us_exp) < V_us_err := V_us_match
  34
  35theorem row_V_cb : abs (V_cb_pred - V_cb_exp) < V_cb_err := V_cb_match
  36
  37theorem row_V_ub : abs (V_ub_pred - V_ub_exp) < V_ub_err := V_ub_match
  38
  39theorem row_vus_eq_geometry : V_us_pred = torsion_overlap - cabibbo_radiative_correction :=
  40  vus_derived
  41
  42theorem row_vcb_eq_geometry : V_cb_pred = edge_dual_ratio := vcb_derived
  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