ChargedLeptonMassScoreCardCert
plain-language theorem explainer
The structure packages five relative-error bounds on the RS-predicted charged-lepton masses at rungs 2, 13 and 19 together with the muon-to-electron and tau-to-electron ratios. A researcher comparing the Recognition Science mass ladder to PDG data cites the certificate to record that all five deviations lie inside the stated 0.3-4 percent windows. The definition simply enumerates the five inequalities using the rs_mass_MeV function and the experimental constants.
Claim. A structure whose fields assert the five inequalities $ |M_{RS}(2) - m_e| / m_e < 0.003 $, $ |M_{RS}(13) - m_μ| / m_μ < 0.04 $, $ |M_{RS}(19) - m_τ| / m_τ < 0.03 $, $ |φ^{11} - m_μ/m_e| / (m_μ/m_e) < 0.04 $ and $ |φ^{17} - m_τ/m_e| / (m_τ/m_e) < 0.03 $, where $M_{RS}(r)$ denotes the Recognition-Science mass formula in MeV evaluated on the indicated lepton rung.
background
The module implements Phase 2 of the lepton-mass verification (P2-LEP). The RS mass formula rs_mass_MeV evaluates the phi-ladder mass expression at lepton rungs 2, 13, 19 with ZOf = 1332 for charged leptons, versus PDG reference masses supplied by the constants m_e_exp := 0.51099895069, m_mu_exp := 105.6583755 and m_tau_exp := 1776.86 together with the derived ratios ratio_mu_e_exp and ratio_tau_e_exp. The Lepton inductive type enumerates the three charged species; the Anchor.tau function supplies the generation torsion values 0, 11, 17 that enter the rung map.
proof idea
The structure is introduced by a direct definition that lists the five field predicates; no lemmas are applied.
why it matters
This certificate is the target of the theorem chargedLeptonMassScoreCardCert_holds, which constructs an explicit inhabitant by substituting the row_* lemmas. It records the numerical agreement between the Recognition-Science phi-ladder (T6 self-similar fixed point, T7 eight-tick octave) and PDG values for the charged leptons, closing one cell of the P2-LEP verification. The open question remains whether the exact mass formula without the stated tolerance bands can be derived from the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.