IndisputableMonolith.Constants.ElectronMass

   1import Mathlib
   2import IndisputableMonolith.Constants
   3import IndisputableMonolith.Masses.Anchor
   4import IndisputableMonolith.Foundation.PhiForcing
   5
   6/-!
   7# C-007: Electron Mass Derivation
   8
   9Formalizes the RS derivation of the electron mass from the φ-ladder.
  10
  11## Registry Item
  12- C-007: What determines the electron mass m_e?
  13
  14## RS Derivation
  15The electron sits on rung r = 2 of the lepton ladder.
  16m_e = E_coh · φ^2 in RS units, where E_coh = φ⁻⁵.
  17Thus m_e_rs = φ^(-3) = φ⁻⁵ · φ^2 (coherence-scaled).
  18-/
  19
  20namespace IndisputableMonolith
  21namespace Constants
  22namespace ElectronMass
  23
  24open Real Constants
  25open Masses.Anchor
  26open Masses.Anchor.Integers
  27
  28/-! ## Definition -/
  29
  30/-- Electron mass in RS units: E_coh · φ^2.
  31    Uses r_lepton "e" = 2 from Anchor. -/
  32noncomputable def m_e_rs : ℝ := Anchor.E_coh * phi ^ (r_lepton "e")
  33
  34/-- m_e_rs = E_coh · φ^2. -/
  35theorem m_e_rs_eq : m_e_rs = E_coh * phi ^ 2 := by
  36  simp only [m_e_rs, r_lepton_values]
  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
  57