gf_matches

proof body

Tactic-mode proof.

 118  -- Numerically verified:
 119  -- fermiConstant = 1.1663787e-5
 120  -- gf_from_mw = sqrt(2) * (2*80.3692/246.22)² / (8*80.3692²)
 121  --            = sqrt(2) / (2*246.22²) ≈ 1.167e-5
 122  -- Relative error ≈ 0.05% << 10%
 123  --
 124  -- Key algebraic identity: gf_from_mw = sqrt(2) / (2 * vev_GeV²)
 125  -- Proof: g = 2*mW/v, so g² = 4*mW²/v²
 126  -- gf_from_mw = sqrt(2) * 4*mW²/v² / (8*mW²) = sqrt(2) / (2*v²)
 127  have h_gf_simplify : gf_from_mw = sqrt 2 / (2 * vev_GeV^2) := by
 128    unfold gf_from_mw weak_coupling_g
 129    have hv : vev_GeV ≠ 0 := by unfold vev_GeV; norm_num
 130    have hm : wBosonMass_GeV ≠ 0 := by unfold wBosonMass_GeV; norm_num
 131    field_simp
 132    ring
 133  -- sqrt(2) bounds: 1.41 < sqrt(2) < 1.42
 134  have h_sqrt2_lower : (1.41 : ℝ) < sqrt 2 := by
 135    have h : (1.41 : ℝ)^2 < 2 := by norm_num
 136    have h_pos : (0 : ℝ) ≤ 1.41 := by norm_num
 137    rw [← sqrt_sq h_pos]
 138    exact sqrt_lt_sqrt (by norm_num) h
 139  have h_sqrt2_upper : sqrt 2 < (1.42 : ℝ) := by
 140    have h : (2 : ℝ) < (1.42 : ℝ)^2 := by norm_num
 141    have h_pos : (0 : ℝ) ≤ 1.42 := by norm_num
 142    rw [← sqrt_sq h_pos]
 143    exact sqrt_lt_sqrt (by positivity) h
 144  -- vev² bounds: 246.22^2 = 60624.2084, so 60624 < vev² < 60625
 145  have h_vev_sq_bounds_lower : (60624 : ℝ) < vev_GeV^2 := by unfold vev_GeV; norm_num
 146  have h_vev_sq_bounds_upper : vev_GeV^2 < (60625 : ℝ) := by unfold vev_GeV; norm_num
 147  -- gf_from_mw bounds: use sqrt(2)/(2*vev²) with bounds on sqrt(2) and vev²
 148  -- For a/b with a > 0: larger b gives smaller result
 149  -- gf_from_mw > sqrt(2) / (2 * 60625) > 1.41 / (2 * 60625)
 150  have h_gf_lower : gf_from_mw > 1.41 / (2 * 60625) := by
 151    rw [h_gf_simplify]
 152    -- sqrt 2 / (2 * vev²) > sqrt 2 / (2 * 60625) since vev² < 60625
 153    have h_denom : 2 * vev_GeV ^ 2 < 2 * 60625 := by linarith [h_vev_sq_bounds_upper]
 154    have h_sqrt_pos : sqrt 2 > 0 := sqrt_pos.mpr (by norm_num : (0 : ℝ) < 2)
 155    have h1 : sqrt 2 / (2 * vev_GeV ^ 2) > sqrt 2 / (2 * 60625) := by
 156      have h_d1_pos : 0 < 2 * vev_GeV ^ 2 := by positivity
 157      have h_d2_pos : 0 < 2 * (60625 : ℝ) := by norm_num
 158      exact div_lt_div_of_pos_left h_sqrt_pos h_d1_pos h_denom
 159    -- sqrt 2 / (2 * 60625) > 1.41 / (2 * 60625) since sqrt 2 > 1.41
 160    have h2 : sqrt 2 / (2 * 60625) > 1.41 / (2 * 60625) := by
 161      exact div_lt_div_of_pos_right h_sqrt2_lower (by norm_num)
 162    linarith
 163  -- gf_from_mw < 1.42 / (2 * 60624) (using sqrt2 < 1.42 and vev² > 60624)
 164  have h_gf_upper : gf_from_mw < 1.42 / (2 * 60624) := by
 165    rw [h_gf_simplify]
 166    -- sqrt 2 / (2 * vev²) < sqrt 2 / (2 * 60624) since vev² > 60624
 167    have h_denom : 2 * 60624 < 2 * vev_GeV ^ 2 := by linarith [h_vev_sq_bounds_lower]
 168    have h_sqrt_pos : sqrt 2 > 0 := sqrt_pos.mpr (by norm_num : (0 : ℝ) < 2)
 169    have h1 : sqrt 2 / (2 * vev_GeV ^ 2) < sqrt 2 / (2 * 60624) := by
 170      have h_d1_pos : 0 < 2 * (60624 : ℝ) := by norm_num
 171      exact div_lt_div_of_pos_left h_sqrt_pos (by positivity) h_denom
 172    -- sqrt 2 / (2 * 60624) < 1.42 / (2 * 60624) since sqrt 2 < 1.42
 173    have h2 : sqrt 2 / (2 * 60624) < 1.42 / (2 * 60624) := by
 174      exact div_lt_div_of_pos_right h_sqrt2_upper (by norm_num)
 175    linarith
 176  -- Numerical evaluation
 177  have h_lower_val : (1.41 : ℝ) / (2 * 60625) > 1.162e-5 := by norm_num
 178  have h_upper_val : (1.42 : ℝ) / (2 * 60624) < 1.172e-5 := by norm_num
 179  -- So gf_from_mw ∈ (1.162e-5, 1.172e-5) and fermiConstant = 1.1663787e-5
 180  -- |diff| < 0.01e-5, relative error < 0.01e-5 / 1.1663787e-5 < 0.01 < 0.1
 181  have h_diff_bound : |fermiConstant - gf_from_mw| < 0.01e-5 := by
 182    rw [abs_lt]
 183    constructor
 184    · -- fermiConstant - gf_from_mw > -0.01e-5
 185      have hg : gf_from_mw < 1.172e-5 := lt_trans h_gf_upper h_upper_val
 186      have hf : fermiConstant = 1.1663787e-5 := rfl
 187      linarith
 188    · -- fermiConstant - gf_from_mw < 0.01e-5
 189      have hg : gf_from_mw > 1.162e-5 := lt_trans h_lower_val h_gf_lower
 190      have hf : fermiConstant = 1.1663787e-5 := rfl
 191      linarith
 192  have h_fc_pos : fermiConstant > 0 := by unfold fermiConstant; norm_num
 193  -- Relative error bound
 194  have h_rel : |fermiConstant - gf_from_mw| / fermiConstant < 0.01e-5 / 1.1663787e-5 := by
 195    exact div_lt_div_of_pos_right h_diff_bound h_fc_pos
 196  have h_ratio : (0.01e-5 : ℝ) / 1.1663787e-5 < 0.01 := by norm_num
 197  linarith
 198-- ... 5 more lines elided ...