`V_cb_geom`

definition

show as: view math explainer →

module: IndisputableMonolith.Physics.CKMGeometry
domain: Physics
line: 63 · 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 63.

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

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.

papers checked against this theorem

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