muonic_smaller
plain-language theorem explainer
The theorem shows that the reciprocal of the muon-electron mass ratio is strictly less than one. This establishes that the muonic Bohr radius is smaller than the electronic one and therefore samples shorter distances inside the proton. Physicists analyzing the proton radius puzzle cite it to justify the advantage of muonic hydrogen spectroscopy. The proof is a one-line wrapper that rewrites the division inequality from positivity and invokes the direct fact that the mass ratio exceeds unity.
Claim. Let $r = m_μ / m_e = φ^{11}$ be the muon-to-electron mass ratio. Then $1/r < 1$.
background
The module develops the proton charge radius from Recognition Science by combining confinement scales with the phi-ladder of lepton masses. The local definition muon_electron_ratio sets this ratio to φ^11, matching the rung difference (electron at rung 2, muon at rung 13). Upstream lemmas from LeptonMassLadder and AnchorPolicy both derive the same equality m_μ/m_e = φ^11 via mass_on_rung and anchor_ratio, while muon_heavier proves the ratio exceeds one and muon_ratio_pos supplies the required positivity.
proof idea
One-line wrapper that rewrites the target inequality via div_lt_one applied to the positivity hypothesis muon_ratio_pos, then closes the goal by exact application of the muon_heavier theorem.
why it matters
The result supplies the elementary inequality needed to argue that muonic measurements probe shorter distances, directly supporting the proton radius estimate and form-factor corrections in the RS_Proton_Radius_Puzzle paper. It sits inside the phi-ladder mass construction (T5 J-uniqueness and T6 fixed-point forcing) and is a prerequisite for leptonic universality statements. No open scaffolding remains; the claim is fully discharged by the mass-ladder theorems.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.