muon_ratio_pos
plain-language theorem explainer
muon_ratio_pos establishes that the muon-electron mass ratio is strictly positive. It is cited in derivations of muonic Bohr radii and proton radius estimates within Recognition Science. The proof is a one-line wrapper that applies the transitivity lemma lt_trans to the positivity of one and the fact that the ratio exceeds one.
Claim. $0 < m_μ / m_e$ (where the ratio equals $φ^{11}$ on the Recognition Science mass ladder).
background
The module computes the proton charge radius from Recognition Science, following the paper RS_Proton_Radius_Puzzle.tex. The muon-electron ratio is supplied by the lepton mass ladder theorem, which states m_μ_RS / m_e_RS = phi^11 via mass_on_rung. The local setting uses the phi-ladder for lepton masses and the J-cost framework imported from JcostCore. Upstream, lt_trans from ArithmeticFromLogic supplies order transitivity on LogicNat, while muon_heavier supplies the strict inequality 1 < ratio.
proof idea
The term proof applies lt_trans directly to one_pos and muon_heavier. No further rewriting or case analysis is required; the two facts chain to yield the desired positivity.
why it matters
It is invoked by muonic_smaller to obtain 1 / muon_electron_ratio < 1, which shows the muonic Bohr radius is smaller and therefore probes shorter distances. This step supports the RS proton radius estimate that combines confinement with form factor corrections. The result sits in the chain from lepton mass ladder (T5 J-uniqueness and phi fixed point) to nuclear scales, closing a basic positivity requirement before radius inequalities.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.