def
definition
V_cb_geom
show as:
view math explainer →
open explainer
Read the cached plain-language explainer.
open lean source
IndisputableMonolith.Physics.CKMGeometry on GitHub at line 63.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
used by
formal source
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.
82
83 pred = 1/24 ≈ 0.04166666...
84 obs = 0.04182
85 err = 0.00085
86 |pred - obs| = |0.04166 - 0.04182| = 0.00016 < 0.00085 ✓
87
88 This is now PROVEN, not axiomatized. -/
89theorem V_cb_match : abs (V_cb_pred - V_cb_exp) < V_cb_err := by
90 simp only [V_cb_pred, V_cb_geom, V_cb_exp, V_cb_err, edge_dual_ratio]
91 norm_num
92
93/-- Bounds on alpha needed for CKM proofs.