Physics Electron Mass

The electron mass

The electron mass is the mass of a single electron, the stable elementary particle that carries one unit of negative electric charge. In the International System of units, its measured value is 0.510998950 MeV/c², where MeV is a unit of energy and c is the speed of light. This number is one of the most precisely known constants in physics: the electron is light, stable, and easy to isolate, so its mass is a reference point for other particle masses and for the energy scales of atomic and nuclear processes.

The standard model of particle physics does not predict the electron mass from first principles. It appears as a free parameter, an input that experiments supply. A structural derivation would mean showing that this specific number follows from a deeper principle rather than being chosen by hand. The electron mass is also connected to the fine-structure constant, which measures the strength of the electromagnetic interaction, through quantum electrodynamics and the electron's anomalous magnetic moment.

In Recognition Science, the framework proposes such a structural derivation. Its library of formal theorems models the electron mass as a ledger fraction, a discrete ratio of counting numbers, with radiative corrections added. The residue, the difference between the structural mass and the observed mass, is expressed as a formula involving the numbers 17, 12, and 11, which the framework identifies with wallpaper groups, cube edges, and passive edges, plus terms in the fine-structure constant. The framework's library proves that this residue lies within a small interval, and that it matches a separate gap-minus-shift quantity to within 0.002, given two unproven hypotheses about the residue's bounds.

This is a hypothesis-driven result, not a theorem. The matching to 0.002 is a conditional proof: it holds if the two hypotheses about the residue's bounds are true. The framework does not derive the electron mass from nothing; it provides a candidate structural explanation and a machine-checked proof of a conditional statement about it. The empirical check against the measured value is a separate matter from the formal derivation.

/-- Bounds on `electron_residue` (currently **hypothesis-driven**).

    With structural_mass ∈ (10856, 10858) and m_obs = 0.510998950:
    electron_residue ∈ (-20.7063, -20.7058) -/
theorem electron_residue_bounds :
  Necessity.electron_residue_lower_hypothesis →
    Necessity.electron_residue_upper_hypothesis →
      (-20.7063 : ℝ) < electron_residue ∧ electron_residue < (-20.7057 : ℝ) :=
by
  intro hlo hhi
  exact ⟨hlo, hhi⟩

/-- Bounds on `electron_residue` (currently **hypothesis-driven**).

    With structural_mass ∈ (10856, 10858) and m_obs = 0.510998950:
    electron_residue ∈ (-20.7063, -20.7058) -/
theorem electron_residue_bounds :
  Necessity.electron_residue_lower_hypothesis →
    Necessity.electron_residue_upper_hypothesis →
      (-20.7063 : ℝ) < electron_residue ∧ electron_residue < (-20.7057 : ℝ) :=
by
  intro hlo hhi
  exact ⟨hlo, hhi⟩

/-- Bounds on `electron_residue` (currently **hypothesis-driven**).

    With structural_mass ∈ (10856, 10858) and m_obs = 0.510998950:
    electron_residue ∈ (-20.7063, -20.7058) -/
theorem electron_residue_bounds :
  Necessity.electron_residue_lower_hypothesis →
    Necessity.electron_residue_upper_hypothesis →
      (-20.7063 : ℝ) < electron_residue ∧ electron_residue < (-20.7057 : ℝ) :=
by
  intro hlo hhi
  exact ⟨hlo, hhi⟩

/-- Bounds on `(gap 1332 - refined_shift)`.

    With gap ∈ (13.953, 13.954) and shift ∈ (34.6590, 34.6593):
    gap - shift ∈ (-20.7063, -20.705) -/
theorem gap_minus_shift_bounds :
  (-20.7063 : ℝ) < gap 1332 - refined_shift ∧ gap 1332 - refined_shift < (-20.705 : ℝ) :=
by
  have h_gap := Necessity.gap_1332_bounds
  have h_shift := Necessity.refined_shift_bounds
  constructor <;> linarith [h_gap.1, h_gap.2, h_shift.1, h_shift.2]

/-- **Theorem (T9)**: The missing shift is approximately the Refined Ledger Fraction.

    The electron residue matches (gap - refined_shift) within interval bounds.

    NOTE: With corrected interval bounds, we can only prove matching to ~0.002.
    The actual values match to ~1e-6 but proving that requires tighter input bounds. -/
theorem electron_mass_ledger_hypothesis :
    Necessity.electron_residue_lower_hypothesis →
      Necessity.electron_residue_upper_hypothesis →
        abs (electron_residue - (gap 1332 - refined_shift)) < 2 / 1000 := by
  intro h_res_lo h_res_hi
  have h_res := electron_residue_bounds h_res_lo h_res_hi
  have h_gap := gap_minus_shift_bounds
  rw [abs_lt]
  constructor <;> linarith [h_res.1, h_res.2, h_gap.1, h_gap.2]

What this page does not claim

This page does not claim that the electron mass is derived from the framework's axioms without any hypotheses. The matching to 0.002 is not claimed as an exact equality; the true values agree to about 1e-6 but the proof only establishes the looser bound. The identification of 17, 12, and 11 with wallpaper groups, cube edges, and passive edges is a definitional choice, not a theorem.

Verify this page

Every tagged claim above names its theorem. To check one yourself rather than trust this page, elaborate the source module with Lean 4 and audit its axiom basis:

$ lake env lean IndisputableMonolith/Physics/ElectronMass.lean
expected axiom basis: [propext, Classical.choice, Quot.sound] (the Lean kernel's standard three; no RS-specific axioms)

A page whose claims cannot be reproduced this way does not ship. In production, every anchor links to the exact declaration in the public source release, and this block carries the build receipt for the page itself.

Derived articles

This page is generated by a question-recursion engine: the questions its answers raise become the next pages. The current agenda, with open targets marked red: