pith. machine review for the scientific record. sign in
theorem

m_e_pos

proved
show as:
view math explainer →
module
IndisputableMonolith.Constants.ElectronMass
domain
Constants
line
40 · github
papers citing
none yet

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.Constants.ElectronMass on GitHub at line 40.

browse module

All declarations in this module, on Recognition.

explainer page

A cached Ask Recognition explainer exists for this declaration.

open explainer

Derivations using this theorem

depends on

used by

formal source

  37  rfl
  38
  39/-- m_e > 0. -/
  40theorem m_e_pos : 0 < m_e_rs := by
  41  unfold m_e_rs
  42  positivity
  43
  44/-! ## C-007 Resolution -/
  45
  46/-- **C-007 Resolution**: The electron mass is determined by φ and the lepton rung.
  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.