theorem
proved
row_vcb_eq_geometry
show as:
view math explainer →
open explainer
Generate a durable explainer page for this declaration.
open lean source
IndisputableMonolith.Physics.CKMElementScoreCard on GitHub at line 42.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
used by
formal source
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
64end IndisputableMonolith.Physics.CKMElementScoreCard