s23_w

formal source

  58
  59/- Auxiliary positive witness using φ-rung sines (keeps algebra simple). -/
  60noncomputable def s12_w : ℝ := V_us
  61noncomputable def s23_w : ℝ := V_cb
  62noncomputable def s13_w : ℝ := V_ub
  63
  64noncomputable def jarlskog_witness : ℝ := s12_w * s23_w * s13_w
  65
  66/-- The witness is strictly positive (grounded in jarlskog_pos). -/
  67theorem jarlskog_witness_pos : jarlskog_witness > 0 := by
  68  have h := MixingDerivation.jarlskog_pos
  69  unfold jarlskog_witness s12_w s23_w s13_w
  70  -- jarlskog_pred = edge_dual_ratio * fine_structure_leakage * torsion_overlap * sin ckm_cp_phase
  71  -- s12 * s23 * s13 = V_us * V_cb * V_ub
  72  -- This matches the terms in jarlskog_pred up to radiative corrections.
  73  unfold V_us_pred V_cb_pred V_ub_pred
  74  unfold edge_dual_ratio fine_structure_leakage torsion_overlap
  75  -- The witness is positive because each component is positive.
  76  have h_us : 0 < V_us_pred := by
  77    -- V_us_pred = torsion_overlap - cabibbo_radiative_correction
  78    unfold V_us_pred torsion_overlap cabibbo_radiative_correction
  79    have h1 := phi_inv3_lower_bound
  80    have h2 := alpha_upper_bound
  81    -- phi^-3 > 0.236, alpha < 0.00731
  82    -- 1.5 * alpha < 1.5 * 0.00731 = 0.010965
  83    -- US > 0.236 - 0.010965 = 0.225035 > 0
  84    linarith
  85  have h_cb : 0 < V_cb_pred := by unfold V_cb_pred; norm_num
  86  have h_ub : 0 < V_ub_pred := by unfold V_ub_pred fine_structure_leakage; exact div_pos Constants.alpha_pos (by norm_num)
  87  exact mul_pos (mul_pos h_us h_cb) h_ub
  88
  89end Physics
  90end IndisputableMonolith