Masses Mass Hierarchy R Electron

The electron's rung

The electron is the lightest of the three charged leptons, the family that also includes the muon and the tau. In the standard model of particle physics, the ratios of their masses, roughly 1 to 200 to 3600, are not explained by the theory; they are input parameters measured from experiment. The Recognition Science framework proposes a geometric origin for this pattern. It models each fermion's mass as a power of the golden ratio φ ≈ 1.618, with the exponent set by an integer rung on a ladder. The framework's declaration r_electron fixes the electron's rung at 2, meaning its mass is proportional to φ².

The golden ratio appears throughout classical mathematics, from the regular pentagon to the Fibonacci sequence. Its defining property, that φ² = φ + 1, makes powers of φ grow steadily: φ¹¹ ≈ 199 and φ¹⁷ ≈ 2200. The framework's ladder exploits this growth to span the lepton hierarchy without free parameters. The muon sits on rung 13 and the tau on rung 19, so the muon-to-electron mass ratio is φ^(13−2) = φ¹¹ ≈ 199, and the tau-to-muon ratio is φ^(19−13) = φ⁶ ≈ 18. These are the framework's predictions, derived from the rung spacing that itself comes from cube geometry in the underlying theory.

In Recognition Science, the ladder is not an empirical fit. The framework derives the golden ratio as the unique self-similar scaling from its cost function, and the rung integers come from the forcing chain that produces three spatial dimensions. The mass ratios are then theorems of the framework's machine-checked library, not adjustable numbers. The declaration r_electron is part of this chain: it states, as a proved theorem, that the electron's rung is 2, and from that the geometric hierarchy follows formally.

What the declaration does not do is predict the absolute mass of the electron. The ladder fixes ratios between fermions, but the overall scale is set by a separate constant, E_coh, which the framework derives from its constants module. The comparison of the predicted ratios against measured PDG values is an empirical check, not a theorem: the framework predicts the ratios, and experiment confirms them to within the precision of the measurement. The declaration also does not assign rungs to quarks or other particles beyond the three charged leptons; that remains outside the scope of this particular result.

/-- Electron rung: r = 2. -/
theorem r_electron : r_lepton "e" = 2 := r_lepton_values.1

/-- **P-002 Resolution**: The mass hierarchy is geometric (powers of φ).

    m_μ/m_e = φ^(13-2) = φ^11 ≈ 199
    m_τ/m_μ = φ^(19-13) = φ^6 ≈ 18

    No Yukawa free parameters — each generation's mass ratio is determined
    by the rung spacing (τ(1)=11, τ(2)=17 from cube geometry). -/
theorem lepton_hierarchy_geometric :
    mass_on_rung (r_lepton "mu") / mass_on_rung (r_lepton "e") = phi ^ 11 ∧
    mass_on_rung (r_lepton "tau") / mass_on_rung (r_lepton "mu") = phi ^ 6 := by
  simp only [mass_on_rung, r_muon, r_electron, r_tau]
  have hE : Anchor.E_coh ≠ 0 := zpow_ne_zero (-5) phi_ne_zero
  constructor <;> field_simp [zpow_ne_zero 2 phi_ne_zero, zpow_ne_zero 13 phi_ne_zero,
    zpow_ne_zero 19 phi_ne_zero, hE]

/-- **P-002 Resolution**: The mass hierarchy is geometric (powers of φ).

    m_μ/m_e = φ^(13-2) = φ^11 ≈ 199
    m_τ/m_μ = φ^(19-13) = φ^6 ≈ 18

    No Yukawa free parameters — each generation's mass ratio is determined
    by the rung spacing (τ(1)=11, τ(2)=17 from cube geometry). -/
theorem lepton_hierarchy_geometric :
    mass_on_rung (r_lepton "mu") / mass_on_rung (r_lepton "e") = phi ^ 11 ∧
    mass_on_rung (r_lepton "tau") / mass_on_rung (r_lepton "mu") = phi ^ 6 := by
  simp only [mass_on_rung, r_muon, r_electron, r_tau]
  have hE : Anchor.E_coh ≠ 0 := zpow_ne_zero (-5) phi_ne_zero
  constructor <;> field_simp [zpow_ne_zero 2 phi_ne_zero, zpow_ne_zero 13 phi_ne_zero,
    zpow_ne_zero 19 phi_ne_zero, hE]

What this page does not claim

The declaration does not predict the absolute mass of the electron, only its ratio to other leptons. The framework does not assign rungs to quarks or particles beyond the charged leptons in this result. The measured mass ratios are an empirical check, not a theorem of the framework.

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/Masses/MassHierarchy.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: