Masses Mass Hierarchy Lepton Mass Increasing

The lepton mass ladder

The electron, muon, and tau are the three charged leptons, the family of particles that includes the electron that orbits atomic nuclei. Their measured masses are strikingly uneven: the muon is about 200 times heavier than the electron, and the tau is roughly 18 times heavier than the muon. A complete theory of particle physics must explain why these ratios are what they are, not merely record them.

Recognition Science offers one answer. In the framework, each fermion sits on a specific rung of the phi-ladder, a discrete sequence of mass values where each step multiplies the previous mass by the golden ratio φ ≈ 1.618. The electron occupies rung 2, the muon rung 13, and the tau rung 19, so their masses are the coherent energy E_coh times φ raised to the rung number: mass = E_coh · φ^r. The rung spacings, 11 steps between electron and muon and 6 between muon and tau, come from cube geometry in the framework. This structure is a definitional choice, a model of how masses arrange themselves, not a derived theorem on its own.

The key theorem, lepton_mass_increasing, proves a simple but necessary consequence: because φ > 1 and the exponents 11 and 6 are positive, both φ^11 and φ^6 exceed 1. In plain language, the mass ratios m_muon/m_electron and m_tau/m_muon are each greater than one, so each successive lepton generation is heavier than the last. The framework's machine-checked library of formal theorems verifies this from the definition of mass_on_rung and the assigned rung numbers. The hierarchy is geometric, not arbitrary: the ratios are exactly φ^11 ≈ 199 and φ^6 ≈ 18, with no free parameters.

In Recognition Science, then, the lepton mass hierarchy is not an unexplained list of numbers but a fixed ladder with a proved upward direction. The theorem establishes the ordering, not the absolute masses. The absolute scale E_coh is a separate constant, and the comparison of these ratios to measured particle data is an empirical check, not part of the formal proof. What the declaration guarantees is the qualitative fact that the ladder climbs, and the quantitative fact that it climbs by exact powers of the golden ratio.

/-- Mass in RS units: E_coh · φ^r where r is the rung. -/
noncomputable def mass_on_rung (r : ℤ) : ℝ :=
  Anchor.E_coh * phi ^ r

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

/-- Muon rung: r = 13 (2 + 11). -/
theorem r_muon : r_lepton "mu" = 13 := r_lepton_values.2.1

/-- Tau rung: r = 19 (2 + 17). -/
theorem r_tau : r_lepton "tau" = 19 := r_lepton_values.2.2

/-- **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]

/-- Mass ratios are > 1 (each generation heavier). -/
theorem lepton_mass_increasing :
    phi ^ 11 > 1 ∧ phi ^ 6 > 1 :=
  ⟨one_lt_zpow₀ one_lt_phi (by norm_num : 0 < (11 : ℤ)),
   one_lt_zpow₀ one_lt_phi (by norm_num : 0 < (6 : ℤ))⟩

What this page does not claim

The theorem does not prove the absolute masses of the leptons, only their ratios. The rung assignments are a model, not a derived consequence, within this declaration. No comparison to experimental particle data is made in this 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/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: