muon_heavier
plain-language theorem explainer
The Recognition Science lepton mass ladder assigns the muon-electron ratio the value φ^11. Researchers modeling muonic hydrogen or testing lepton universality would invoke this ordering to compare Bohr radii. The proof is a direct reduction of the inequality to the fact that the golden ratio exceeds one, using the power monotonicity lemma.
Claim. $1 < φ^{11}$, where $φ$ is the golden ratio and the exponent 11 is the rung difference between the electron and muon states on the Recognition Science mass ladder.
background
In the ProtonRadius module the muon-electron mass ratio is introduced as the direct definition φ raised to the eleventh power. This encodes the eleven-rung separation on the phi-ladder between the electron (rung 2) and muon (rung 13) that follows from the general mass formula yardstick · φ^(rung - 8 + gap(Z)). The upstream theorem in LeptonMassLadder establishes the same ratio by unfolding mass_on_rung and simplifying the exponent difference via field_simp and zpow_sub.
proof idea
The proof unfolds the definition of the ratio to obtain φ^11 and then applies the lemma one_lt_pow₀, which states that a > 1 implies 1 < a^n for positive integer n. The hypothesis phi_gt_one supplies the base inequality and norm_num discharges the concrete exponent 11.
why it matters
This ordering result is invoked directly by muonic_smaller to conclude that the muonic Bohr radius is smaller than the electronic one, and by muon_ratio_pos to establish positivity. It supplies the strict inequality step required for proton-radius estimates that combine confinement scales with form-factor corrections in the Recognition Science framework. The rung difference of 11 is consistent with the phi-ladder construction that descends from the J-uniqueness and self-similar fixed-point steps of the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.