row_electron_rel
plain-language theorem explainer
The declaration bounds the relative deviation of the Recognition Science electron mass prediction at rung 2 from the experimental value below 0.3 percent. Researchers auditing lepton mass ladders in the RS framework would reference this when certifying scorecard entries. The proof consists of a one-line wrapper that invokes the corresponding relative error theorem from the quark scorecard module.
Claim. $|rs_mass_MeV(Lepton, 2) - m_{e,exp}| / m_{e,exp} < 0.003$, where $rs_mass_MeV$ applies the phi-ladder formula to the lepton sector at rung 2 and $m_{e,exp}$ is the PDG electron mass 0.51099895069 MeV.
background
The module develops phase 2 predictions for charged lepton masses using the RS mass formula. rs_mass_MeV takes a sector and rung to return the predicted mass in MeV via the expression 2 to the B_pow of the sector times phi to the power of negative 5 times phi to r0 of sector times phi to the rung, divided by one million. The Lepton type from CubeFaceUniversality enumerates the six lepton flavors. This row reuses the electron relative error already proved in the quark scorecard as row_electron_pct, which itself reduces to Verification.electron_relative_error. The local theoretical setting places the RS predictions for rungs 2, 13 and 19 with ZOf equal to 1332 against the experimental references in Verification, with the falsifier being a PDG update that moves any mass outside the percent bands.
proof idea
One-line wrapper that applies row_electron_pct from the QuarkScoreCard module.
why it matters
This bound populates the electron field in the charged lepton mass scorecard certificate, which is the theorem chargedLeptonMassScoreCardCert_holds asserting the certificate is nonempty. It contributes to the partial theorem status for P2-LEP in the Recognition Science framework, relying on the phi-ladder and the forcing chain steps T5 through T8. The residual gap and anchor issues noted in the module doc remain open questions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.