Masses Mass Hierarchy R Muon

The muon's rung

The muon is a heavier cousin of the electron, the second of the three charged leptons. In the standard model of particle physics, its mass is an input: experiments measure it, and the theory takes the number as given. The Recognition Science framework proposes an alternative, that the mass of each lepton is set by a position on a discrete ladder of values. Each rung of that ladder multiplies the previous one by the golden ratio φ, about 1.618. A particle on rung 13 is therefore φ^11 times heavier than a particle on rung 2, since 13 minus 2 is 11.

The framework's machine-checked library of formal theorems records this assignment in a declaration called r_muon. The declaration establishes that the muon sits on rung 13 of the φ-ladder, with the electron on rung 2 and the tau on rung 19. From those positions, a proved theorem derives the mass ratios: the muon is φ^11 times the electron's mass, about 199, and the tau is φ^6 times the muon's, about 18. The hierarchy is geometric, each generation heavier than the last, and the ratios are fixed by the rung spacing rather than by free parameters.

What r_muon does not do is predict the muon's absolute mass. The ladder sets ratios between particles; it does not fix the overall scale E_coh that anchors the bottom rung. The declaration also does not claim that the rung numbers 2, 13, and 19 are derived from first principles within this file. Those integers are assigned, and the docstring notes that the spacing between generations, 11 and 17, comes from cube geometry, but that derivation lives elsewhere in the framework. The theorem here proves the consequences of the assignment, not the assignment itself.

In plain terms, the declaration is a precise bookkeeping statement: given the φ-ladder and the assigned rungs, the muon's mass relative to the electron is forced to be φ^11. The empirical check against the measured mass ratio is a separate step, not part of the theorem. The framework's claim is that the hierarchy has a geometric structure, and r_muon is the formal anchor for the muon's place in it.

/-- Muon rung: r = 13 (2 + 11). -/
theorem r_muon : r_lepton "mu" = 13 := r_lepton_values.2.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]

/-- 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 absolute mass of the muon, since the overall scale E_coh is not fixed in this declaration. The origin of the assigned rung numbers 2, 13, and 19, which are inputs here and derived elsewhere. An empirical match to the measured muon mass, which is a separate check and not part of the 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: