`electron_structural_mass_forced`

proved

show as: view math explainer →

module: IndisputableMonolith.RRF.Physics.ElectronMass.Defs
domain: RRF
line: 78 · github
papers citing: none yet

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.RRF.Physics.ElectronMass.Defs on GitHub at line 78.

browse module

All declarations in this module, on Recognition.

explainer page

A cached Ask Recognition explainer exists for this declaration.

open explainer

depends on

used by

formal source

  75             = 2^(-22) * φ^51
  76
  77    Proof: Direct computation shows φ^(-5) * φ^62 * φ^(-6) = φ^51. -/
  78theorem electron_structural_mass_forced :
  79    electron_structural_mass = (2 : ℝ) ^ (-22 : ℤ) * phi ^ (51 : ℤ) := by
  80  unfold electron_structural_mass lepton_yardstick E_coh lepton_B lepton_R0 electron_rung
  81  have hne : (phi : ℝ) ≠ 0 := phi_ne_zero
  82  have h1 : phi ^ (-5 : ℤ) * phi ^ (62 : ℤ) = phi ^ (57 : ℤ) := by
  83    rw [← zpow_add₀ hne]; norm_num
  84  have h2 : phi ^ (57 : ℤ) * phi ^ (-6 : ℤ) = phi ^ (51 : ℤ) := by
  85    rw [← zpow_add₀ hne]; norm_num
  86  have hsub : ((2 : ℤ) - 8 : ℤ) = (-6 : ℤ) := by norm_num
  87  simp only [hsub, h1, mul_assoc]
  88  rw [h2]
  89
  90end ElectronMass
  91end Physics
  92end IndisputableMonolith

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.