electron_charge

formal source

  35def electron_rung : ℤ := 2
  36
  37/-- Electron charge q = -1. -/
  38def electron_charge : ℤ := -1
  39
  40/-! ## Structural Mass Derivation -/
  41
  42/-- The Yardstick (Sector Scale): Y = 2^B · E_coh · φ^R0. -/
  43noncomputable def lepton_yardstick : ℝ :=
  44  (2 : ℝ) ^ lepton_B * E_coh * phi ^ lepton_R0
  45
  46/-- The Structural Mass: m_struct = Y · φ^(r-8). -/
  47noncomputable def electron_structural_mass : ℝ :=
  48  lepton_yardstick * phi ^ (electron_rung - 8)
  49
  50/-- Dimensionless Structural Ratio to E_coh. -/
  51noncomputable def electron_structural_ratio : ℝ :=
  52  electron_structural_mass / E_coh
  53
  54/-! ## The Residue (The Break) -/
  55
  56/-- Observed Electron Mass (in MeV, placeholder for ratio matching).
  57    Ref: 0.510998950 MeV. -/
  58def mass_ref_MeV : ℝ := 0.510998950
  59
  60/-- The Residue Δ = log_φ(m_obs / m_struct).
  61    Value from audit: -20.70596. -/
  62noncomputable def electron_residue : ℝ :=
  63  Real.log (mass_ref_MeV / electron_structural_mass) / Real.log phi
  64
  65/-- The Electron Mass Formula (T9). -/
  66noncomputable def predicted_electron_mass : ℝ :=
  67  electron_structural_mass * phi ^ (gap 1332 - refined_shift)
  68