theorem proved tactic proof

`alphaG_pred_eq`

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

formal statement (Lean)

  91theorem alphaG_pred_eq :
  92    row_alphaG_pred = electron_structural_mass ^ 2 * phi ^ (10 : ℝ) / Real.pi := by

proof body

Tactic-mode proof.

  93  have hc : hbar * c = hbar := hbar_c_eq_hbar
  94  rw [row_alphaG_pred, hc]
  95  have h1 : G * electron_structural_mass ^ 2 / hbar
  96        = (G / hbar) * electron_structural_mass ^ 2 := by
  97    have hh : hbar ≠ 0 := ne_of_gt hbar_pos
  98    field_simp [hh]
  99  rw [h1, G_div_hbar]
 100  ring
 101

depends on (15)

Lean names referenced from this declaration's body.

G in IndisputableMonolith.Constants decl_use
hbar in IndisputableMonolith.Constants decl_use
hbar_pos in IndisputableMonolith.Constants decl_use
G in IndisputableMonolith.Constants.Codata decl_use
hbar in IndisputableMonolith.Constants.Codata decl_use
hbar_pos in IndisputableMonolith.Constants.Codata decl_use
G in IndisputableMonolith.Cost.FunctionalEquation decl_use
G in IndisputableMonolith.Gravity.JCostInflaton decl_use
hbar in IndisputableMonolith.Information.ComputationLimitsStructure decl_use
G_div_hbar in IndisputableMonolith.Masses.AlphaGScoreCard decl_use
hbar_c_eq_hbar in IndisputableMonolith.Masses.AlphaGScoreCard decl_use
row_alphaG_pred in IndisputableMonolith.Masses.AlphaGScoreCard decl_use
electron_structural_mass in IndisputableMonolith.Physics.ElectronMass.Defs decl_use
hbar in IndisputableMonolith.Quantum.EntanglementEntropy decl_use
electron_structural_mass in IndisputableMonolith.RRF.Physics.ElectronMass.Defs decl_use