electron_charge

formal source

 138theorem electron_rung_eq : electron_rung = 2 := rfl
 139
 140/-- Electron charge q = -1 (in units of e). -/
 141def electron_charge : ℤ := -1
 142
 143/-! ## Structural Mass Derivation -/
 144
 145/-- The Yardstick (Sector Scale): Y = 2^B · E_coh · φ^R0.
 146    Using derived values: Y = 2^(-22) · φ^(-5) · φ^62. -/
 147noncomputable def lepton_yardstick : ℝ :=
 148  (2 : ℝ) ^ lepton_B * E_coh * phi ^ lepton_R0
 149
 150/-- Alternative using explicit values (for compatibility). -/
 151noncomputable def lepton_yardstick_explicit : ℝ :=
 152  (2 : ℝ) ^ (-22 : ℤ) * phi ^ (-5 : ℤ) * phi ^ (62 : ℤ)
 153
 154/-- PROOF: The derived yardstick equals the explicit form. -/
 155theorem lepton_yardstick_eq_explicit :
 156    lepton_yardstick = lepton_yardstick_explicit := by
 157  simp only [lepton_yardstick, lepton_yardstick_explicit, E_coh_eq,
 158             lepton_B_eq, lepton_R0_eq]
 159
 160/-- The Structural Mass: m_struct = Y · φ^(r-8). -/
 161noncomputable def electron_structural_mass : ℝ :=
 162  lepton_yardstick * phi ^ (electron_rung - (octave_period : ℤ))
 163
 164/-- Dimensionless Structural Ratio to E_coh. -/
 165noncomputable def electron_structural_ratio : ℝ :=
 166  electron_structural_mass / E_coh
 167
 168/-! ## The Residue (The Break) -/
 169
 170/-- Observed Electron Mass (in MeV, placeholder for ratio matching).
 171    Ref: 0.510998950 MeV.