lepton_masses_from_ladder
plain-language theorem explainer
Lepton mass ratios in RS units are fixed by the phi-ladder: muon over electron equals phi to the eleventh power, tau over electron phi to the seventeenth, and tau over muon phi to the sixth. A physicist modeling lepton spectra from Recognition Science would cite this when verifying the P-011 derivation. The proof is a direct conjunction of three prior ratio theorems obtained by exponent subtraction on the mass definitions.
Claim. Let $m_e$, $m_μ$, $m_τ$ denote the RS-unit masses of the electron, muon and tau lepton. Then $m_μ/m_e = φ^{11} ∧ m_τ/m_e = φ^{17} ∧ m_τ/m_μ = φ^6$.
background
The LeptonMassLadder module places the electron at rung 2, muon at rung 13 and tau at rung 19 on the phi-ladder, with each mass given by mass_on_rung r = E_coh · φ^r. This implements the RS derivation m_e ∝ φ^2, m_μ ∝ φ^13, m_τ ∝ φ^19. Upstream results include the definitions m_e_rs, m_mu_rs, m_tau_rs together with the separate theorems muon_electron_ratio and tau_electron_ratio that reduce each ratio to the appropriate power of phi via zpow_sub after unfolding.
proof idea
The term proof packages the three ratio theorems muon_electron_ratio, tau_electron_ratio and tau_muon_ratio into a single conjunction. Each supporting theorem unfolds the mass_on_rung definitions, cancels the common E_coh factor, and applies Real.zpow_sub followed by norm_num to obtain the exact exponent difference.
why it matters
The theorem completes the P-011 resolution by supplying the full set of lepton mass ratios required by the Recognition Science framework. It depends on the phi-ladder construction in MassHierarchy and the individual ratio lemmas, confirming that rung spacings of 11 and 17 arise from the cube geometry in the forcing chain. No downstream uses are recorded yet, leaving open its integration into broader mass hierarchy proofs.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.