m_mu_pos
plain-language theorem explainer
The theorem asserts that the muon mass on the Recognition Science phi-ladder is strictly positive. Researchers deriving lepton masses from the electron base rung would cite this when confirming the hierarchy remains in the positive reals. The proof unfolds m_mu_rs to mass_on_rung 13 and applies the positivity tactic to the resulting product.
Claim. $0 < E_0 phi^{13}$ where $E_0$ is the coherence energy scale and $phi$ is the golden-ratio fixed point.
background
The LeptonMassLadder module places lepton masses on the phi-ladder with the muon assigned rung 13. The upstream mass_on_rung definition sets the mass at integer rung r to Anchor.E_coh multiplied by phi raised to r. The sibling definition m_mu_rs specializes this to rung 13, giving E_coh · φ^13 in RS-native units. The module doc states the RS derivation m_e ∝ φ^2, m_μ ∝ φ^13, m_τ ∝ φ^19 together with the approximate ratios m_μ/m_e ≈ φ^11 ≈ 199.
proof idea
The term proof is a one-line wrapper. It unfolds m_mu_rs and mass_on_rung, reducing the goal to positivity of Anchor.E_coh * phi ^ 13. The positivity tactic then discharges the inequality directly from the positivity of the coherence scale and the exponential.
why it matters
The result anchors the muon entry in the P-011 lepton-mass hierarchy, ensuring the phi-ladder formula stays positive before ratio calculations such as muon-electron ratio. It sits inside the forcing chain after T6 (phi fixed point) and supports the eight-tick octave structure. No open scaffolding remains; the claim is fully discharged.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.