alphaG_pred_closed

proof body

Tactic-mode proof.

 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 : ℝ))]
 133  rw [row_alphaG_pred, hc, hsq]
 134  have hsplit :
 135      G * ((2 : ℝ) ^ (-(44 : ℤ)) * (phi : ℝ) ^ (102 : ℝ)) / hbar
 136        = (G / hbar) * ((2 : ℝ) ^ (-(44 : ℤ)) * (phi : ℝ) ^ (102 : ℝ)) := by
 137    have hh : hbar ≠ 0 := ne_of_gt hbar_pos
 138    field_simp [hh]
 139  rw [hsplit, G_div_hbar]
 140  have hmerge : phi ^ (10 : ℝ) * phi ^ (102 : ℝ) = phi ^ (112 : ℝ) := by
 141    simpa [mul_comm] using hφ112
 142  field_simp [Real.pi_ne_zero, h0, Real.rpow_pos_of_pos phi_pos, h2pos, Real.rpow_pos_of_pos phi_pos (102 : ℝ),
 143    Real.rpow_pos_of_pos phi_pos (10 : ℝ), Real.rpow_pos_of_pos phi_pos (112 : ℝ)]
 144  -- After clearing `π`, identify `φ^{10}·φ^{102} = φ^{112}`.
 145  exact hmerge
 146
 147/-! ## Bracket: single-φ function (avoids a fake independence assumption) -/
 148