m_e_pos
plain-language theorem explainer
The theorem asserts positivity of the electron mass expressed via the phi-ladder in RS units. Researchers deriving lepton mass ratios within the Recognition Science hierarchy cite it to anchor the baseline before computing muon and tau values. The proof is a one-line wrapper that unfolds the mass definition and applies the positivity tactic.
Claim. $0 < E_0 phi^2$, where $E_0$ is the coherence energy scale and $phi$ the self-similar fixed point.
background
The LeptonMassLadder module formalizes lepton masses on the phi-ladder with the electron assigned rung 2. The auxiliary definition mass_on_rung r returns E_coh times phi raised to rung r. This matches the module statement that m_e scales as phi^2, m_mu as phi^13, and m_tau as phi^19. Upstream results supply the mass_on_rung definition from MassHierarchy and parallel positivity statements from ElectronMass.
proof idea
The proof unfolds m_e_rs to the mass_on_rung expression at rung 2, then invokes the positivity tactic on the resulting product of positive factors.
why it matters
This positivity statement supports the C-007 resolution that the electron mass equals E_coh times phi^2 with no free parameters. It feeds the electron_mass_derived theorem that pairs positivity with the explicit form. The result sits inside the mass formula on the phi-ladder and connects to the T6 fixed-point construction.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.