row_tau_rel
plain-language theorem explainer
The declaration shows that the Recognition Science mass formula at lepton rung 19 produces a tau mass within 3 percent of the PDG experimental value. A researcher assembling lepton mass predictions or verifying the phi-ladder scorecard would cite this row when building the charged-lepton certificate. The proof is a direct one-line reference to the matching percentage theorem already established in the quark scorecard module.
Claim. The relative error between the RS-predicted tau mass at rung 19 and the experimental tau mass satisfies $ | rs_mass_MeV(Lepton, 19) - m_τ_exp | / m_τ_exp < 0.03 $.
background
The ChargedLeptonMassScoreCard module addresses Phase 2 (P2-LEP) predictions for the charged lepton masses e, μ, τ. It applies the integer-rung mass formula rs_mass_MeV on rungs 2, 13, 19 with ZOf = 1332 for charged leptons, then compares the results to the PDG reference values m_e_exp, m_mu_exp, m_tau_exp defined in Verification. The Lepton inductive type from CrossDomain.CubeFaceUniversality enumerates the six lepton flavors, while rs_mass_MeV is defined as (2 : ℝ)^(B_pow s) * phi^(-5) * phi^(r0 s) * phi^r / 1000000. Upstream, row_tau_pct states that the tau mass lies within 3 percent of PDG and is proved via tau_relative_error.
proof idea
The proof is a one-line wrapper that applies row_tau_pct from the QuarkScoreCard module.
why it matters
This row is collected into chargedLeptonMassScoreCardCert_holds, which constructs the Nonempty ChargedLeptonMassScoreCardCert by bundling the relative-error statements for electron, muon, tau, and the two mass ratios. It supplies the tau entry in the P2-LEP phase of the Recognition Science mass scorecard, where masses follow the phi-ladder with rung and gap adjustments. The module records that the same gap/anchor residual present for quarks persists if the exact exponential form rs_mass_MeV = M0 * exp((rung-8+gap) log φ) is required.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.