electron_relative_error
plain-language theorem explainer
The theorem establishes that the Recognition Science mass prediction for the electron at rung 2 differs from the experimental PDG value by less than 0.3 percent. Particle physicists verifying the phi-ladder mass formula against data would cite this bound when certifying the lepton sector. The proof equates the RS expression to an auxiliary prediction, imports the established numerical interval on that prediction, and reduces the relative-error inequality to an interval comparison discharged by linear arithmetic.
Claim. Let $m_{RS}$ denote the Recognition Science prediction for the electron mass in MeV at rung 2 and let $m_e$ be the experimental value 0.51099895069 MeV. Then $|m_{RS} - m_e| / m_e < 0.003$.
background
In the Masses.Verification module experimental masses are imported constants while RS predictions are computed from the phi-ladder. The function rs_mass_MeV (Sector, r) evaluates $2^{B_{pow} s} · ϕ^{-5} · ϕ^{r0 s} · ϕ^r / 10^6$, with $B_{pow} = -22$ and $r0 = 62$ for leptons, giving the explicit formula $m(Lepton, r) = ϕ^{57+r} / (2^{22} · 10^6)$ MeV. The experimental electron mass is the constant 0.51099895069. The auxiliary result electron_pred_eq equates the rung-2 RS value to electron_pred while electron_mass_bounds supplies the tight interval 0.5098 < electron_pred < 0.5102.
proof idea
The proof rewrites the RS mass term via electron_pred_eq, obtains the interval via electron_mass_bounds, and records positivity of the experimental constant by unfolding and norm_num. It then applies div_lt_iff₀ and abs_lt, unfolds the experimental constant, and reduces both sides of the target inequality to linear comparisons solved directly by nlinarith on the two bounds.
why it matters
This bound supplies the electron percentage error required by mass_verification_cert_exists to inhabit MassVerificationCert and by phi_ladder_verified to certify the full lepton ladder to the stated tolerances; it is invoked verbatim by row_electron_pct. Within the Recognition framework it closes one verification step for the phi-ladder mass formula in the lepton sector, consistent with the integer-rung construction derived from the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.