mass_verification_cert_exists
plain-language theorem explainer
The theorem asserts existence of a certificate confirming that RS lepton mass predictions fall inside narrow PDG intervals for the electron, muon and tau, with relative errors below 0.3 percent, 4 percent and 3 percent respectively. A physicist checking Recognition Science mass formulas against experiment would cite the result. The proof is a direct term construction that assembles the certificate record from pre-proved bound and error lemmas.
Claim. There exists a structure $C$ such that $0.5098 < m_e^pred < 0.5102$, $101.49 < m_μ^pred < 101.57$, $1821 < m_τ^pred < 1823$ (MeV), $|m_e^RS - m_e^exp|/m_e^exp < 0.003$, $|m_μ^RS - m_μ^exp|/m_μ^exp < 0.04$, $|m_τ^RS - m_τ^exp|/m_τ^exp < 0.03$, and the mass-ratio errors satisfy $|φ^{11} - r_{μe}^exp|/r_{μe}^exp < 0.04$ together with $|φ^{17} - r_{τe}^exp|/r_{τe}^exp < 0.03$.
background
The module treats experimental lepton masses as quarantined imported constants rather than RS-derived quantities. The lepton-sector formula is given as $m(Lepton,r)=φ^{57+r}/(2^{22}×10^6)$ MeV. MassVerificationCert is the record type that packages the three interval checks, the three relative-error bounds, and the two ratio-error bounds. Upstream results supply the rung definition (a natural-number selector) and the RS-native Mass abbreviation (the reals).
proof idea
The proof is a term-mode record construction. It supplies the interval fields directly from the lemmas electron_mass_bounds, muon_mass_bounds and tau_mass_bounds, and the percentage fields from the corresponding relative-error lemmas for the three masses and the two ratios.
why it matters
The declaration closes the machine-checked comparison of phi-ladder predictions against PDG data for the lepton sector. It supports the Recognition Science claim that integer rungs on the golden-ratio ladder reproduce observed masses to within a few percent. The result sits after the mass-anchor derivations and before any extension to hadrons; it touches the T6 self-similar fixed-point step and the mass formula yardstick × φ^(rung-8+gap(Z)).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.