m2_approx_bounds

formal source

 714
 715/-- PROVEN: Bounds on m2_approx = sqrt(7.53e-5) ≈ 0.00868 eV
 716    Proof: 0.0086² = 7.396e-5 < 7.53e-5 < 7.744e-5 = 0.0088² -/
 717lemma m2_approx_bounds : (0.0086 : ℝ) < m2_approx ∧ m2_approx < (0.0088 : ℝ) := by
 718  simp only [m2_approx, dm2_21_exp]
 719  constructor
 720  · -- 0.0086 < sqrt(7.53e-5)
 721    have h1 : (0.0086 : ℝ)^2 < 7.53e-5 := by norm_num
 722    have h_pos : (0 : ℝ) < 7.53e-5 := by norm_num
 723    have h_sqrt_pos : 0 < Real.sqrt (7.53e-5) := Real.sqrt_pos.mpr h_pos
 724    have h_086_pos : (0 : ℝ) ≤ 0.0086 := by norm_num
 725    rw [← Real.sqrt_sq h_086_pos]
 726    exact Real.sqrt_lt_sqrt (sq_nonneg _) h1
 727  · -- sqrt(7.53e-5) < 0.0088
 728    have h1 : (7.53e-5 : ℝ) < 0.0088^2 := by norm_num
 729    have h_pos : (0 : ℝ) ≤ 7.53e-5 := by norm_num
 730    have h_088_pos : (0 : ℝ) < 0.0088 := by norm_num
 731    rw [← Real.sqrt_sq (le_of_lt h_088_pos)]
 732    exact Real.sqrt_lt_sqrt h_pos h1
 733
 734/-- m2 matches the -58 rung to within tolerance (< 0.001 eV).
 735
 736    Proof: From nu2_pred_bounds and m2_approx_bounds,
 737    |0.0082 - 0.0087| ≈ 0.0005 < 0.001 ✓ -/
 738theorem nu2_match : abs (predicted_mass_eV rung_nu2 - m2_approx) < 0.001 := by
 739  have h_pred := nu2_pred_bounds
 740  have h_m2 := m2_approx_bounds
 741  -- pred ∈ (0.0081, 0.0083), m2 ∈ (0.0086, 0.0088)
 742  -- Worst case: |0.0081 - 0.0088| = 0.0007 < 0.001 ✓
 743  rw [abs_lt]
 744  constructor <;> linarith [h_pred.1, h_pred.2, h_m2.1, h_m2.2]
 745
 746/-- **CERTIFICATE: Neutrino Deep Ladder**
 747    Packages the proofs for atmospheric (m3) and solar (m2) neutrino mass matches. -/