jarlskog_match

proof body

Tactic-mode proof.

 286  -- External verification: J ≈ (1/24) * (α/2) * (φ⁻³) * 1 ≈ 3.03e-5
 287  -- |3.03e-5 - 3.08e-5| = 0.05e-5 < 0.6e-5 ✓
 288  -- Keep `Constants.alpha` opaque (avoid simp unfolding), and only simplify sin(pi/2)=1.
 289  have hsin : Real.sin ckm_cp_phase = (1 : ℝ) := by
 290    simp [ckm_cp_phase, Real.sin_pi_div_two]
 291  -- Rewrite the prediction into a clean closed form.
 292  have hj :
 293      jarlskog_pred = Constants.alpha * (phi ^ (-3 : ℤ)) / 48 := by
 294    -- jarlskog_pred = (1/24) * (alpha/2) * phi^(-3) * 1
 295    unfold jarlskog_pred fine_structure_leakage torsion_overlap
 296    -- replace sin(pi/2)
 297    simp only [hsin]
 298    -- expand the rational factor 1/24 (as ℝ) and rearrange
 299    simp only [edge_dual_ratio]
 300    ring_nf
 301  -- Use the rewritten form for all bounds.
 302  rw [hj]
 303  -- Bound α and φ^(-3).
 304  have hα_lo := CKMGeometry.alpha_lower_bound
 305  have hα_hi := CKMGeometry.alpha_upper_bound
 306  have hφ3_lo : (0.2360 : ℝ) < phi ^ (-3 : ℤ) := CKMGeometry.phi_inv3_lower_bound
 307  have hφ3_hi : phi ^ (-3 : ℤ) < (0.2361 : ℝ) := CKMGeometry.phi_inv3_upper_bound
 308  -- Convert the goal to a simple enclosing interval: 2.48e-5 < J < 3.68e-5.
 309  rw [abs_lt]
 310  constructor
 311  · -- lower: 3.08e-5 - 0.6e-5 < J
 312    -- Use a conservative product lower bound.
 313    have hJ_lo : (0.00729 : ℝ) * (0.2360 : ℝ) / 48 < Constants.alpha * (phi ^ (-3 : ℤ)) / 48 := by
 314      have h48 : (0 : ℝ) < (48 : ℝ) := by norm_num
 315      have hmul : (0.00729 : ℝ) * (0.2360 : ℝ) < Constants.alpha * (phi ^ (-3 : ℤ)) := by
 316        nlinarith [hα_lo, hφ3_lo]
 317      exact div_lt_div_of_pos_right hmul h48
 318    have hnum : (2.48e-5 : ℝ) < (0.00729 : ℝ) * (0.2360 : ℝ) / 48 := by norm_num
 319    have : (2.48e-5 : ℝ) < Constants.alpha * (phi ^ (-3 : ℤ)) / 48 := lt_trans hnum hJ_lo
 320    linarith
 321  · -- upper: J < 3.08e-5 + 0.6e-5
 322    have hJ_hi : Constants.alpha * (phi ^ (-3 : ℤ)) / 48 < (0.00731 : ℝ) * (0.2361 : ℝ) / 48 := by
 323      have h48 : (0 : ℝ) < (48 : ℝ) := by norm_num
 324      have hmul : Constants.alpha * (phi ^ (-3 : ℤ)) < (0.00731 : ℝ) * (0.2361 : ℝ) := by
 325        nlinarith [hα_hi, hφ3_hi]
 326      exact div_lt_div_of_pos_right hmul h48
 327    have hnum : (0.00731 : ℝ) * (0.2361 : ℝ) / 48 < (3.68e-5 : ℝ) := by norm_num
 328    have : Constants.alpha * (phi ^ (-3 : ℤ)) / 48 < (3.68e-5 : ℝ) := lt_trans hJ_hi hnum
 329    linarith
 330