MassVerificationCert
plain-language theorem explainer
MassVerificationCert bundles eight numerical predicates confirming that Recognition Science lepton mass predictions fall inside experimental intervals for the electron, muon, and tau, with relative errors below 0.3 percent, 4 percent, and 3 percent, plus ratio checks against powers of phi. A physicist auditing the phi-ladder mass formula against PDG data would cite this certificate. The declaration is a plain structure definition that directly assembles the interval and error bounds with no lemmas invoked.
Claim. A structure whose fields assert $0.5098 < m_e^{pred} < 0.5102$, $101.49 < m_μ^{pred} < 101.57$, $1821 < m_τ^{pred} < 1823$ (MeV), relative errors $|m^{RS}(Lepton,2) - m_e^{exp}|/m_e^{exp} < 0.003$ and analogously for muon and tau with thresholds 0.04 and 0.03, together with $|φ^{11} - r_{μe}^{exp}|/r_{μe}^{exp} < 0.04$ and $|φ^{17} - r_{τe}^{exp}|/r_{τe}^{exp} < 0.03$.
background
The module supplies machine-verified numerical checks for lepton masses under the integer-rung formula m(Lepton, r) = φ^{57+r} / (2^{22} × 10^6) MeV. The Lepton inductive type enumerates the charged leptons electron, muon, tau. The Constants structure from the CPM Law of Existence supplies the golden ratio φ. Upstream definitions compute electron_pred = φ^{59}/(2^{22}×10^6) and fix the experimental anchors m_e_exp ≈ 0.510999 MeV, m_mu_exp ≈ 105.658 MeV, m_tau_exp ≈ 1776.86 MeV.
proof idea
The structure is defined directly by listing the eight field predicates on the predicted masses, experimental values, and ratio expressions; it functions as a one-line wrapper collecting the interval and relative-error conditions with no lemmas or tactics applied.
why it matters
MassVerificationCert supplies the carrier type for the theorem mass_verification_cert_exists, which exhibits an explicit inhabitant to certify numerical agreement between RS predictions and experiment in the lepton sector. It supports the mass formula on the phi-ladder that follows from the J-uniqueness (T5) and self-similar fixed point (T6) steps in the forcing chain. The module is quarantined from the certified core because experimental inputs remain external constants.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.