row_tau_electron_ratio
plain-language theorem explainer
Row tau electron ratio asserts that the experimental tau-to-electron mass ratio lies within three percent of phi to the seventeenth power. Researchers verifying Recognition Science mass predictions for charged leptons would cite this bound when assembling the scorecard certificate. The proof is a one-line wrapper that invokes the percentage-error theorem already established in the quark scorecard module.
Claim. $ |phi^{17} - (m_τ / m_e)_{exp}| / (m_τ / m_e)_{exp} < 0.03 $ where the experimental ratio is taken from PDG values and phi denotes the Recognition Science self-similar fixed point.
background
Module Masses.ChargedLeptonMassScoreCard assembles relative error bounds for the electron, muon, and tau masses predicted on the phi-ladder at rungs 2, 13, and 19 with ZOf = 1332. Upstream row_tau_electron_ratio_pct states that the tau-electron PDG mass ratio matches phi^17 within 3 percent, and ratio_tau_e_exp is defined as m_tau_exp / m_e_exp. The local setting is Phase 2 P2-LEP verification of charged lepton masses against PDG references, carrying the same gap/anchor residual noted for the quark sector.
proof idea
The proof is a one-line wrapper that applies row_tau_electron_ratio_pct from the QuarkScoreCard module.
why it matters
This bound is collected into chargedLeptonMassScoreCardCert_holds to certify the full set of relative errors for the charged leptons. It contributes to the mass formula verification on the phi-ladder and the eight-tick octave structure. The module notes the partial theorem status and the remaining gap/anchor issue if rs_mass_MeV must be expressed as M0 * exp((rung-8+gap) log phi).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.