`V_us_exp`

definition

show as: view math explainer →

module: IndisputableMonolith.Physics.CKMGeometry
domain: Physics
line: 48 · github
papers citing: none yet

open explainer

Generate a durable explainer page for this declaration.

open lean source

IndisputableMonolith.Physics.CKMGeometry on GitHub at line 48.

browse module

All declarations in this module, on Recognition.

explainer page

Tracked in the explainer inventory; generation is lazy so crawlers do not trigger LLM jobs.

open explainer

used by

formal source

  45
  46/-! ## Experimental Values (PDG 2022) -/
  47
  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

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.