jarlskog_summary

formal source

  47  j_matches_experiment : jarlskog ≈ j_value
  48
  49/-- Dimensionless inevitability when supplied with phenomenological data. -/
  50def jarlskog_summary (facts : CKMPhenomenology) : Prop :=
  51  jarlskog > 0 ∧ jarlskog ≈ facts.j_value
  52
  53lemma jarlskog_summary_of_facts (facts : CKMPhenomenology)
  54    (hpos : jarlskog > 0 := facts.j_positive)
  55    (hexp : jarlskog ≈ facts.j_value := facts.j_matches_experiment) :
  56    jarlskog_summary facts :=
  57  ⟨hpos, hexp⟩
  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