pith. sign in
module module moderate

IndisputableMonolith.Masses.LeptonMassLadder

show as:
view Lean formalization →

The LeptonMassLadder module supplies explicit RS-unit definitions for the electron, muon, and tau masses via the phi-ladder. Researchers deriving numerical mass ratios or testing the fermion hierarchy would cite these when moving from the abstract MassHierarchy to concrete lepton values. The module consists of direct definitions that instantiate the mass formula without additional lemmas or proofs.

claimThe electron mass is $m_e = E_{coh} · φ^2$ in RS units; the muon and tau masses follow by shifting rungs on the same phi-ladder, with all values anchored to the canonical constants $E_{coh}$ and $τ_0 = 1$.

background

This module belongs to the Masses domain and imports the phi-forcing result establishing φ as the self-similar fixed point under J-cost, the Anchor module supplying parameter-free canonical constants, and the MassHierarchy module that formalizes P-002. The phi-ladder supplies the discrete scaling rule for fermion masses: yardstick times φ raised to an integer rung offset. The local setting is the RS derivation of charged-lepton masses from the J-cost ledger, with the electron placed at the lowest rung E_coh · φ².

proof idea

this is a definition module, no proofs

why it matters in Recognition Science

The module instantiates the P-002 fermion mass hierarchy for the three charged leptons, supplying the concrete expressions that downstream ratio calculations (muon-electron, tau-electron) rely on. It closes the step from the abstract phi-ladder in MassHierarchy to explicit lepton masses inside the Recognition Science framework.

scope and limits

depends on (4)

Lean names referenced from this declaration's body.

declarations in this module (10)