muon_ratio_undershoot
The theorem shows that the golden ratio to the eleventh power lies strictly below the experimental muon-to-electron mass ratio. A physicist checking Recognition Science lepton mass predictions against PDG data would cite it to establish the undershoot before invoking the full phi-ladder formula. The proof is a one-line linarith wrapper that combines the bound phi^11 less than 200 with the experimental interval 206.76 to 206.77.
claim$phi^{11} < m_mu^{exp} / m_e^{exp}$, where phi denotes the golden ratio and the right-hand side is the experimental muon-to-electron mass ratio.
background
The module compares Recognition Science mass predictions to PDG experimental values while treating the latter as imported constants rather than derived quantities. For the lepton sector the integer-rung formula is m(Lepton, r) = phi^{57+r} / (2^{22} * 10^6) in MeV. The experimental ratio is defined as m_mu_exp divided by m_e_exp and is bounded by the theorem 206.76 less than ratio less than 206.77. The auxiliary lemma phi11_lt establishes that Constants.phi raised to the eleventh power is less than 200, using the identification of phi with the golden ratio together with known bounds on phi^8 and phi^3.
proof idea
One-line wrapper that applies linarith to the two facts phi^11 less than 200 and the lower endpoint of the experimental ratio interval.
why it matters in Recognition Science
The result anchors the verification that the phi-ladder prediction for the muon lies below the observed ratio, consistent with the self-similar fixed point phi forced at T6 of the Unified Forcing Chain. It sits inside the quarantined experimental comparison block of the Masses.Verification module and supports the broader claim that Recognition Science reproduces lepton mass ratios to within the stated precision band without deriving the experimental numbers themselves.
scope and limits
- Does not derive the experimental mass ratio from Recognition Science axioms.
- Does not assert equality between phi^11 and the ratio.
- Does not compute the full predicted muon mass in MeV.
- Does not address higher-generation leptons or hadrons.
formal statement (Lean)
229theorem muon_ratio_undershoot :
230 Constants.phi ^ (11 : ℕ) < ratio_mu_e_exp := by
proof body
One-line wrapper that applies linarith.
231 linarith [phi11_lt, ratio_mu_e_exp_bounds.1]
232