jarlskog_pos

formal source

 328    have : Constants.alpha * (phi ^ (-3 : ℤ)) / 48 < (3.68e-5 : ℝ) := lt_trans hJ_hi hnum
 329    linarith
 330
 331theorem jarlskog_pos : jarlskog_pred > 0 := by
 332  -- J is product of positive quantities: (1/24) * (α/2) * φ^(-3) * sin(π/2)
 333  -- All factors are positive, so J > 0
 334  -- Prove positivity without unfolding `Constants.alpha` into its formula.
 335  unfold jarlskog_pred fine_structure_leakage torsion_overlap ckm_cp_phase
 336  -- Replace sin(pi/2) with 1 (proved in a goal with no `alpha`, so no simp-unfold risk).
 337  have hsin_eq : Real.sin (Real.pi / 2) = (1 : ℝ) := Real.sin_pi_div_two
 338  -- We now have `Real.sin (Real.pi / 2)` in the goal; rewrite it away.
 339  rw [hsin_eq]
 340  have hratio : (0 : ℝ) < (edge_dual_ratio : ℝ) := by
 341    -- edge_dual_ratio = 1/24 as a rational cast to ℝ
 342    simp [edge_dual_ratio]
 343  have hα : (0 : ℝ) < Constants.alpha / 2 := by
 344    have hα0 : (0 : ℝ) < Constants.alpha := by linarith [CKMGeometry.alpha_lower_bound]
 345    have h2 : (0 : ℝ) < (2 : ℝ) := by norm_num
 346    exact div_pos hα0 h2
 347  have hφ : (0 : ℝ) < phi ^ (-3 : ℤ) := by
 348    exact zpow_pos phi_pos (-3)
 349  -- Combine positivity (by successive multiplication).
 350  have h1 : (0 : ℝ) < (edge_dual_ratio : ℝ) * (Constants.alpha / 2) := mul_pos hratio hα
 351  have h2 : (0 : ℝ) < (edge_dual_ratio : ℝ) * (Constants.alpha / 2) * (phi ^ (-3 : ℤ)) :=
 352    mul_pos h1 hφ
 353  -- With sin(pi/2)=1, the goal is exactly `0 < ...`.
 354  simpa [mul_assoc] using h2
 355
 356end MixingDerivation
 357end Physics
 358end IndisputableMonolith