tau_ratio_overshoot
plain-language theorem explainer
The experimental tau-to-electron mass ratio lies strictly below phi to the seventeenth power. Researchers verifying Recognition Science lepton mass predictions against PDG data would reference this bound. A single linarith tactic closes the proof by combining the lower bound on phi^17 with the upper experimental bound on the ratio.
Claim. Let $r = m_τ^{exp} / m_e^{exp}$ denote the experimental mass ratio. Then $r < φ^{17}$.
background
The module compares RS mass predictions for leptons against PDG experimental values, treating the latter as imported constants rather than derived quantities. The lepton mass formula uses the phi-ladder with B_pow = -22 and r0 = 62, giving m(Lepton, r) = φ^{57+r} / (2^{22} × 10^6) in MeV. The declaration uses the golden-ratio constant phi from the Constants structure in LawOfExistence, along with the experimental ratio defined as m_tau_exp / m_e_exp. Upstream, phi17_gt establishes 3569 < phi^{17} via phi_eq_goldenRatio and phi_pow8_gt, while ratio_tau_e_exp_bounds proves 3477 < ratio_tau_e_exp < 3478 by direct norm_num on the imported masses.
proof idea
One-line wrapper that applies linarith to phi17_gt and the right-hand side of ratio_tau_e_exp_bounds.
why it matters
The result anchors the tau-electron comparison inside the lepton-sector verification chain, confirming that the experimental ratio sits below the phi^{17} threshold used in the RS mass ladder. It supports the broader claim that predicted masses remain consistent with PDG data without violating the phi-power bounds from the forcing chain. No downstream theorems currently depend on it.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.