row_alphaG_pred

formal source

  46
  47/-! ## Re-exported row aliases -/
  48
  49noncomputable def row_alphaG_pred : ℝ := G * electron_structural_mass ^ 2 / (hbar * c)
  50
  51theorem row_alphaG_pred_eq : row_alphaG_pred = G * electron_structural_mass ^ 2 / (hbar * c) := rfl
  52
  53/-! ## Helper algebra (native units) -/
  54
  55private theorem c_eq_one' : c = 1 := rfl
  56
  57private theorem hbar_c_eq_hbar : hbar * c = hbar := by
  58  rw [c_eq_one', mul_one]
  59
  60private theorem G_div_hbar : G / hbar = phi ^ (10 : ℝ) / Real.pi := by
  61  have hG : G = 1 / (Real.pi * hbar) := by
  62    unfold G lambda_rec ell0 c
  63    simp
  64  have hh0 : hbar ≠ 0 := ne_of_gt hbar_pos
  65  have h1 : G / hbar = 1 / (Real.pi * hbar ^ 2) := by
  66    rw [hG]
  67    field_simp [Real.pi_ne_zero, hh0]
  68  have h2 : hbar ^ 2 = phi ^ (-(10 : ℝ)) := by
  69    rw [hbar_eq_phi_inv_fifth, pow_two]
  70    have hs : (-(5 : ℝ)) + (-(5 : ℝ)) = -(10 : ℝ) := by ring
  71    rw [← Real.rpow_add phi_pos, hs]
  72  -- `G/ħ = 1/(π·ħ²) = 1/(π·φ^{-10}) = φ^{10}/π`.
  73  rw [h1, h2]
  74  have hphiInv10 : 0 < phi ^ (-(10 : ℝ)) := Real.rpow_pos_of_pos phi_pos (-(10 : ℝ))
  75  have hden : (Real.pi : ℝ) * phi ^ (-(10 : ℝ)) ≠ 0 := by
  76    nlinarith [Real.pi_pos, hphiInv10]
  77  -- `1 = φ^{10} · φ^{-10}`.
  78  have h1over : (1 : ℝ) = phi ^ (10 : ℝ) * phi ^ (-(10 : ℝ)) := by
  79    have h10 : (10 : ℝ) + (-(10 : ℝ)) = 0 := by ring