cabibbo_parameter

formal source

  50In RS, λ = φ^{-(τ₁ − τ₀)/some_scale}. The generation torsion
  51provides the hierarchy directly. -/
  52
  53noncomputable def cabibbo_parameter : ℝ := phi ^ (-(11 : ℤ))
  54
  55theorem cabibbo_parameter_pos : 0 < cabibbo_parameter := by
  56  unfold cabibbo_parameter
  57  exact zpow_pos phi_pos _
  58
  59noncomputable def rs_V_us : ℝ := cabibbo_parameter
  60noncomputable def rs_V_cb : ℝ := cabibbo_parameter ^ 2
  61noncomputable def rs_V_ub : ℝ := cabibbo_parameter ^ 3
  62
  63theorem ckm_hierarchy :
  64    rs_V_ub < rs_V_cb ∧ rs_V_cb < rs_V_us := by
  65  unfold rs_V_ub rs_V_cb rs_V_us
  66  have hc := cabibbo_parameter_pos
  67  have hc1 : cabibbo_parameter < 1 := by
  68    unfold cabibbo_parameter
  69    rw [zpow_neg, zpow_natCast]
  70    exact inv_lt_one_of_one_lt (by nlinarith [one_lt_phi, sq_nonneg phi,
  71      show phi ^ 11 = phi ^ 8 * phi ^ 3 from by ring])
  72  constructor
  73  · nlinarith [sq_nonneg cabibbo_parameter]
  74  · nlinarith [sq_nonneg cabibbo_parameter]
  75
  76/-! ## Unitarity from Ledger Conservation
  77
  78CKM unitarity (V†V = I) is forced by ledger conservation:
  79every quark transition must be accounted for in the double-entry ledger. -/
  80
  81theorem ckm_unitarity_structural :
  82    rs_V_us ^ 2 + rs_V_cb ^ 2 + rs_V_ub ^ 2 < 1 := by
  83  unfold rs_V_us rs_V_cb rs_V_ub