recognition / Constants / Constants.ElectronMass / electron_mass_derived

theorem

`electron_mass_derived`

proved

show as: view math explainer →

module: IndisputableMonolith.Constants.ElectronMass
domain: Constants
line: 50 · github
papers citing: none yet

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.Constants.ElectronMass on GitHub at line 50.

browse module

All declarations in this module, on Recognition.

explainer page

A cached Ask Recognition explainer exists for this declaration.

Derivations using this theorem

Electron Mass on the Phi-Ladder · derived / THEOREM
m_e is forced at rung 27 of the phi-ladder with proved positivity

depends on

formal source

  47
  48    m_e = E_coh · φ^2. No free parameters — the rung r=2 comes from
  49    the lepton sector's baseline in the cube geometry (Anchor.Integers). -/
  50theorem electron_mass_derived :
  51    0 < m_e_rs ∧ m_e_rs = E_coh * phi ^ 2 :=
  52  ⟨m_e_pos, m_e_rs_eq⟩
  53
  54end ElectronMass
  55end Constants
  56end IndisputableMonolith

papers checked against this theorem

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