ratio_tau_e_exp
plain-language theorem explainer
The definition supplies the experimental PDG tau-to-electron mass ratio for direct insertion into verification scorecards. Researchers auditing Recognition Science lepton predictions against data cite this ratio when testing the phi^17 scaling. It is realized as a one-line division of two imported experimental constants.
Claim. The experimental tau-to-electron mass ratio is defined as $m_τ^{exp} / m_e^{exp}$, where the values are the PDG constants 1776.86 MeV and 0.51099895069 MeV.
background
The module compares Recognition Science mass predictions to PDG 2024 data. Experimental masses are imported constants, quarantined from the certified surface and not derived from the unified forcing chain. The lepton sector uses the integer-rung formula $m(Lepton, r) = φ^{57+r} / (2^{22} × 10^6)$ in MeV, with B_pow = -22 and r0 = 62. Upstream constants fix m_e_exp at 0.51099895069 and m_tau_exp at 1776.86.
proof idea
One-line definition that divides the experimental tau mass constant by the experimental electron mass constant.
why it matters
This definition feeds the ChargedLeptonMassScoreCardCert structure, which requires |phi^17 - ratio_tau_e_exp| / ratio_tau_e_exp < 0.03, and the MassVerificationCert bounds. It supports the downstream theorem tau_electron_ratio_error that certifies the 3 percent match to the phi-ladder prediction. The ratio arises because the tau and electron occupy rungs differing by 17 steps on the phi-ladder.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.