def
definition
V_cb_exp
show as:
view math explainer →
open explainer
Generate a durable explainer page for this declaration.
open lean source
IndisputableMonolith.Physics.CKMGeometry on GitHub at line 51.
browse module
All declarations in this module, on Recognition.
explainer page
used by
formal source
48def V_us_exp : ℝ := 0.22500
49def V_us_err : ℝ := 0.00067
50
51def V_cb_exp : ℝ := 0.04182
52def V_cb_err : ℝ := 0.00085
53
54def V_ub_exp : ℝ := 0.00369
55def V_ub_err : ℝ := 0.00011
56
57/-! ## Theoretical Predictions -/
58
59/-- V_ub is half the fine-structure constant (fine_structure_leakage). -/
60noncomputable def V_ub_pred : ℝ := fine_structure_leakage
61
62/-- V_cb geometric ratio: 1/vertex_edge_slots = 1/24. -/
63def V_cb_geom : ℚ := edge_dual_ratio
64
65/-- V_cb is the inverse of twice the total edge count (1/24). -/
66noncomputable def V_cb_pred : ℝ := (V_cb_geom : ℝ)
67
68/-- V_us is the golden projection (torsion_overlap) minus a radiative correction. -/
69noncomputable def V_us_pred : ℝ := torsion_overlap - cabibbo_radiative_correction
70
71/-! ## Geometric Derivation -/
72
73/-- V_cb derives from cube edge geometry: 1/(2 * 12) = 1/24. -/
74theorem V_cb_from_cube_edges :
75 V_cb_geom = 1 / (2 * cube_edges 3) := by
76 simp only [V_cb_geom, edge_dual_ratio, cube_edges]
77 norm_num
78
79/-! ## Verification Theorems -/
80
81/-- V_cb matches within 1 sigma.