gf_matches

formal source

 113    The derivation is: G_F = sqrt(2) * g² / (8 * mW²) where g = 2*mW/v.
 114    Simplifying: G_F = sqrt(2) / (2 * v²).
 115    With v = 246.22 GeV: G_F ≈ 1.167e-5 GeV⁻², matching PDG value 1.166e-5. -/
 116theorem gf_matches :
 117    |fermiConstant - gf_from_mw| / fermiConstant < 0.1 := by
 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