theorem
proved
tactic proof
jarlskog_pos
show as:
view Lean formalization →
formal statement (Lean)
331theorem jarlskog_pos : jarlskog_pred > 0 := by
proof body
Tactic-mode proof.
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