alphaG_pred_closed

formal source

  99  rw [h1, G_div_hbar]
 100  ring
 101
 102theorem alphaG_pred_closed :
 103    row_alphaG_pred = ((2 : ℝ) ^ (-(44 : ℤ)) * phi ^ (112 : ℝ)) / Real.pi := by
 104  have hme : electron_structural_mass = (2 : ℝ) ^ (-(22 : ℤ)) * phi ^ (51 : ℤ) := electron_structural_mass_forced
 105  have h2n : (2 : ℝ) ≠ 0 := by norm_num
 106  have hA2 : ((2 : ℝ) ^ (-(22 : ℤ))) ^ 2 = (2 : ℝ) ^ (-(44 : ℤ)) := by
 107    rw [pow_two, ← zpow_add₀ h2n]
 108    norm_num
 109  have h0 : (phi : ℝ) ≠ 0 := phi_ne_zero
 110  have hBz : (phi : ℝ) ^ (51 : ℤ) * (phi : ℝ) ^ (51 : ℤ) = (phi : ℝ) ^ (102 : ℤ) := by
 111    rw [← zpow_add₀ h0]
 112    norm_num
 113  have hφsq : ((phi : ℝ) ^ (51 : ℤ)) ^ 2 = (phi : ℝ) ^ (102 : ℤ) := by
 114    rw [pow_two]
 115    exact hBz
 116  have hsq : (electron_structural_mass) ^ 2 = (2 : ℝ) ^ (-(44 : ℤ)) * (phi : ℝ) ^ (102 : ℝ) := by
 117    rw [hme, pow_two]
 118    have hre :
 119        ((2 : ℝ) ^ (-(22 : ℤ)) * phi ^ (51 : ℤ)) * ((2 : ℝ) ^ (-(22 : ℤ)) * phi ^ (51 : ℤ))
 120          = ((2 : ℝ) ^ (-(22 : ℤ))) ^ 2 * ((phi : ℝ) ^ (51 : ℤ)) ^ 2 := by
 121      ring
 122    rw [hre, hA2, hφsq]
 123    have hΦ : (phi : ℝ) ^ (102 : ℤ) = (phi : ℝ) ^ (102 : ℝ) := by
 124      -- integer `zpow` and real `rpow` with an `Int` exponent agree on `ℝ`.
 125      simp [zpow_ofNat, phi]
 126    rw [hΦ]
 127  have h112 : (102 : ℝ) + (10 : ℝ) = (112 : ℝ) := by norm_cast
 128  have hφ112 : (phi : ℝ) ^ (102 : ℝ) * (phi : ℝ) ^ (10 : ℝ) = (phi : ℝ) ^ (112 : ℝ) := by
 129    rw [← Real.rpow_add phi_pos, h112]
 130  have hc : hbar * c = hbar := hbar_c_eq_hbar
 131  have h2pos : (0 : ℝ) < (2 : ℝ) ^ (-(44 : ℤ)) := by
 132    simpa [zpow_pos (by norm_num : (0 : ℝ) < (2 : ℝ))]