Masses Smverification Tauon Rung Minus Electron Rung

The tauon-electron mass gap

In the Standard Model of particle physics, the tauon is the heaviest of the three charged leptons, with a measured mass of about 1776.9 MeV/c², compared to the electron's 0.511 MeV/c². The ratio of these masses is roughly 3477, a number that has no simple explanation in the Standard Model itself. Recognition Science (RS) offers a framework where particle masses are not free parameters but positions on a discrete ladder, and the declaration tauon_rung_minus_electron_rung establishes a precise fact about that ladder.

The framework models each fermion as occupying a rung, an integer index on a mass ladder. The mass law is m(particle) = yardstick(Sector) × φ^(r - 8 + gap(Z)), where φ is the golden ratio (approximately 1.618), r is the rung, and the yardstick and gap terms come from cube geometry and charge structure. The declaration proves that for the tauon and electron, the difference in their rungs is exactly 17: r_lepton "tau" - r_lepton "e" = 17. This is a theorem, machine-checked in the framework's library of formal theorems, derived from the definitions of r_lepton, the tau constant, and cube geometry constants.

The consequence is a prediction for the tauon-to-electron mass ratio: m_τ/m_e ≈ φ¹⁷ ≈ 3571. The measured ratio is 3477, an agreement to about 4-5%. This is an empirical check, not a theorem; the framework's mass law is proved, but the comparison against PDG 2024 values is stated as a hypothesis with documented experimental values. The framework also proves the analogous gap for the muon: r_lepton "mu" - r_lepton "e" = 11, giving m_μ/m_e ≈ φ¹¹ ≈ 199.0, against the measured 206.8.

What the declaration does not claim is just as important. It does not prove the absolute masses of the tauon or electron; those require the calibration constant E_coh ≈ 0.0901 eV, which is not derived in this declaration. It does not claim the mass ratio is exactly φ¹⁷; the 4-5% discrepancy is acknowledged and the comparison is tagged as a hypothesis. It does not derive the quark mass gaps, which require gap corrections and agree less well with experiment. The declaration is a structural fact about the framework's internal ladder, a proved step in a larger verification effort, not a complete derivation of the tauon's mass from first principles.

theorem tauon_rung_minus_electron_rung :
    r_lepton "tau" - r_lepton "e" = 17 := by
  simp only [r_lepton, tau, Anchor.W, Anchor.E_passive, passive_field_edges,
             cube_edges, active_edges_per_tick, D, wallpaper_groups]
  norm_num

theorem muon_rung_minus_electron_rung :
    r_lepton "mu" - r_lepton "e" = 11 := by
  simp only [r_lepton, tau, Anchor.E_passive, passive_field_edges,
             cube_edges, active_edges_per_tick, D, wallpaper_groups]
  norm_num

def fermionMass (f : Fermion) : ℝ :=
  predict_mass (fermionSector f) (fermionRung f) (fermionZ f)

def pdg_tauon_MeV : ℝ := 1776.9

What this page does not claim

This declaration does not prove the absolute mass of the tauon or electron. This declaration does not claim the tauon-electron mass ratio is exactly φ¹⁷; the 4-5% discrepancy is acknowledged. This declaration does not derive quark mass gaps, which require additional gap corrections.

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/SMVerification.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: