chargedLeptonMassScoreCardCert_holds
plain-language theorem explainer
The theorem asserts existence of a certificate confirming that Recognition Science mass predictions for the electron, muon and tau satisfy the listed relative-error tolerances against experimental values, together with the two predicted mass ratios. A physicist comparing RS phi-ladder outputs to PDG data would cite the result when documenting the lepton scorecard. The proof is a direct term that assembles the certificate from five already-proved relative-error statements.
Claim. There exists a certificate $C$ such that $|rs_mass_{MeV}(Lepton,2)-m_e|/m_e<0.003$, $|rs_mass_{MeV}(Lepton,13)-m_μ|/m_μ<0.04$, $|rs_mass_{MeV}(Lepton,19)-m_τ|/m_τ<0.03$, $|φ^{11}-(m_μ/m_e)|/(m_μ/m_e)<0.04$, and $|φ^{17}-(m_τ/m_e)|/(m_τ/m_e)<0.03$.
background
The module treats Phase 2 lepton-mass predictions. The function rs_mass_MeV supplies the Recognition Science mass in MeV on the phi-ladder at lepton rungs 2, 13 and 19 with ZOf=1332. The structure ChargedLeptonMassScoreCardCert packages five relative-error bounds: three on individual masses and two on the ratios φ^11 and φ^17. Upstream, the tau function from Anchor supplies the generation torsion values 0, 11 and 17 that fix the rung offsets for the three generations.
proof idea
The proof is a one-line term-mode construction. It instantiates the certificate structure by supplying the five row theorems row_electron_rel, row_muon_rel, row_tau_rel, row_muon_electron_ratio and row_tau_electron_ratio directly into the corresponding fields.
why it matters
The declaration certifies the charged-lepton half of the mass scorecard, placing the RS predictions inside the stated percent bands. It parallels the quark scorecard and completes the partial theorem status noted in the module documentation. The result sits inside the broader mass-formula verification that uses the phi-ladder and the gap(Z) correction; the module records that exact equality rs_mass_MeV = M0 * exp((rung-8+gap)log φ) remains open.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.