Masses Lepton Mass Ladder

Lepton mass ladder

The lepton mass ladder is the pattern in which the electron, muon, and tau masses sit on powers of the golden ratio phi. In Recognition Science the ladder is not a fitted table but a consequence of a shared rung structure: each lepton mass is assigned to a rung, and the rung number fixes the mass as a power of phi. The electron sits on rung 2, the muon on rung 13, and the tau on rung 19, so their masses are proportional to phi squared, phi to the 13th, and phi to the 19th respectively.

The module LeptonMassLadder formalizes these assignments as definitions and then proves the ratios that follow. The muon to electron ratio is phi to the 11th, about 199. The tau to electron ratio is phi to the 17th, about 3571. The tau to muon ratio is phi to the 6th. These three ratio statements are established as theorems in Lean, so the ladder's internal consistency is a checked fact rather than a numerical coincidence.

The ladder's rung spacing is fixed by cube geometry, with the muon and tau at spacings 11 and 17 above the electron. What the module establishes in plain language is that the three lepton masses are not independent: once the electron mass and the rung positions are given, the muon and tau masses are forced as exact powers of phi. The comparison to measured particle masses is an empirical check, not part of the theorem.

MODEL m_e_rs · m_mu_rs · m_tau_rs · IndisputableMonolith/Masses/LeptonMassLadder.lean

THEOREM muon_electron_ratio · IndisputableMonolith/Masses/LeptonMassLadder.lean

THEOREM tau_electron_ratio · IndisputableMonolith/Masses/LeptonMassLadder.lean

THEOREM tau_muon_ratio · IndisputableMonolith/Masses/LeptonMassLadder.lean

What this page does not claim

Not a derivation of the absolute electron mass from first principles. Not an empirical claim that measured lepton masses match the phi ratios; that comparison is outside the theorem. Not a statement about the physical origin of the rung assignments.

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