row_electron_pct
plain-language theorem explainer
The theorem establishes that the Recognition Science mass formula for the electron at rung 2 differs from the PDG experimental value by a relative error strictly less than 0.003. Researchers validating phi-ladder mass predictions against precision data would cite this bound when checking sub-percent accuracy for the lightest charged lepton. The proof is a direct one-line application of the pre-established electron_relative_error lemma.
Claim. $ | rs_mass_MeV(Lepton, 2) - m_e^{exp} | / m_e^{exp} < 0.003 $
background
The QuarkScoreCard module consolidates existing theorem-grade results on fermion masses under the Recognition Science phi-ladder without deriving new physics. It records ZOf assignments (276 for up quarks, 24 for down quarks, 1332 for charged leptons) and notes that equal-Z fermions obey pure phi-power anchor ratios, while flagging the missing gap(ZOf) correction for absolute mass matches. The rs_mass_MeV function computes the predicted mass in MeV from the Verification module; m_e_exp is the PDG experimental electron mass. Upstream structures include J-cost convexity from PhiForcingDerived.of and the forcing of three generations plus 24 chiral flavors from SpectralEmergence.of.
proof idea
The proof is a one-line wrapper that applies the electron_relative_error lemma from the Verification module.
why it matters
This bound is invoked by row_electron_rel in ChargedLeptonMassScoreCard and by quarkScoreCardCert_holds to populate the lepton entry in the scorecard certificate. It completes the phase-0 lepton row of the PHYSICAL_DERIVATION_PLAN by showing sub-percent agreement for the electron on the phi-ladder. The result sits inside the T5-T8 forcing chain and the eight-tick octave, yet the module explicitly leaves absolute quark masses open pending the RSBridge.Anchor equivalence theorem.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.