nu3_pred_bounds

proof body

Tactic-mode proof.

 624  simp only [predicted_mass_eV_legacy, rung_nu3, MeV_to_eV, legacy_mass_display_calibration]
 625  have h_sm := ElectronMass.Necessity.structural_mass_bounds
 626  have h_phi54_gt := IndisputableMonolith.Numerics.phi_neg54_gt
 627  have h_phi54_lt := IndisputableMonolith.Numerics.phi_neg54_lt
 628  have h_phi_eq : phi = Real.goldenRatio := rfl
 629  rw [h_phi_eq]
 630  have hpos_sm : (0 : ℝ) < electron_structural_mass := by
 631    have h := h_sm.1
 632    linarith
 633  have hpos_phi : (0 : ℝ) < Real.goldenRatio ^ (-54 : ℤ) := by
 634    have h := h_phi54_gt
 635    linarith
 636  constructor
 637  · -- 0.055 < structural_mass * φ^(-54) * 1e6
 638    -- Lower bound: 10856 * 5.181e-12 * 1e6 = 0.05626... > 0.055
 639    calc (0.055 : ℝ) < (10856 : ℝ) * (5.181e-12 : ℝ) * (1e6 : ℝ) := by norm_num
 640      _ < electron_structural_mass * (5.181e-12 : ℝ) * (1e6 : ℝ) := by nlinarith [h_sm.1]
 641      _ < electron_structural_mass * Real.goldenRatio ^ (-54 : ℤ) * (1e6 : ℝ) := by nlinarith [h_phi54_gt, hpos_sm]
 642  · -- structural_mass * φ^(-54) * 1e6 < 0.058
 643    -- Upper bound: 10858 * 5.185e-12 * 1e6 = 0.05629... < 0.058
 644    calc electron_structural_mass * Real.goldenRatio ^ (-54 : ℤ) * (1e6 : ℝ)
 645        < (10858 : ℝ) * Real.goldenRatio ^ (-54 : ℤ) * (1e6 : ℝ) := by nlinarith [h_sm.2, hpos_phi]
 646      _ < (10858 : ℝ) * (5.185e-12 : ℝ) * (1e6 : ℝ) := by nlinarith [h_phi54_lt]
 647      _ < (0.058 : ℝ) := by norm_num
 648
 649/-- PROVEN: Bounds on m3_approx = sqrt(2.453e-3) ≈ 0.0495 eV
 650    Proof: 0.049² = 0.002401 < 0.002453 < 0.0025 = 0.050² -/