module module moderate

`IndisputableMonolith.Verification.MassComparison`

Verification module that records PDG-style experimental rest masses and one-sigma uncertainties for the electron, muon, tau, and light quarks u,d,s. Downstream mass-ladder checks cite these constants when comparing Recognition Science predictions to data. Content is pure numeric definitions; no theorems are proved here.

claimFixed experimental anchors $m_e^{\mathrm{exp}}, m_\mu^{\mathrm{exp}}, m_\tau^{\mathrm{exp}}, m_u^{\mathrm{exp}}, m_d^{\mathrm{exp}}, m_s^{\mathrm{exp}}$ (MeV) together with their one-sigma uncertainties $\sigma$, for use in RS mass-ladder residual checks.

background

Recognition Science places particle masses on a $\varphi$-ladder: a yardstick times $\varphi^{r-8+\mathrm{gap}(Z)}$. The Model-layer module Masses.Anchor derives the parameter-free RS constants; this Verification module supplies the experimental side of the comparison only.

Imports pull $\varphi$-interval bounds, the lepton-generation definition layer (T10), and the RS time quantum $\tau_0=1$ tick from Constants. Nothing here claims agreement with data; the numbers are reference values (e.g. electron mass $0.51099895069(16)$ MeV) against which derived ladder outputs can be scored.

Sibling constants cover the three charged leptons and the three light quarks, each paired with an explicit sigma, so residual and $\chi^2$-style checks stay fully explicit in Lean.

proof idea

Definition module, no proofs. Each experimental mass and sigma is introduced as a numeric constant (or abbrev) with a short doc-comment stating the PDG-style value in MeV. Structure is a flat catalogue keyed by species; no lemmas, no tactics, no sorry.

why it matters in Recognition Science

Closes the data side of the RS mass-verification pipeline. Derived ladder masses from Masses.Anchor and lepton-generation definitions need fixed experimental targets; without this catalogue, residual theorems cannot be stated. Sits in the Verification domain rather than the forcing chain (T0–T8) or the RCL, and currently has no recorded downstream Lean dependents in the graph, so it functions as a leaf reference table for paper-level or external comparison scripts.

scope and limits

Does not derive or prove any RS mass formula.
Does not claim experimental agreement or compute residuals.
Does not cover heavy quarks, neutrinos, or gauge bosons.
Does not update values automatically from external PDG feeds.
Does not encode unit conversions beyond the stated MeV anchors.

depends on (4)

Lean names referenced from this declaration's body.

IndisputableMonolith.Constants module_import
IndisputableMonolith.Masses.Anchor module_import
IndisputableMonolith.Numerics.Interval.PhiBounds module_import
IndisputableMonolith.Physics.LeptonGenerations.Defs module_import

declarations in this module (42)

def m_e_exp L49
def m_e_exp_sigma L50
def m_mu_exp L53
def m_mu_exp_sigma L54
def m_tau_exp L57
def m_tau_exp_sigma L58
def m_u_exp L61
def m_u_exp_sigma L62
def m_d_exp L65
def m_d_exp_sigma L66
def m_s_exp L69
def m_s_exp_sigma L70
def m_c_exp L73
def m_c_exp_sigma L74
def m_b_exp L77
def m_b_exp_sigma L78
def m_t_exp L81
def m_t_exp_sigma L82
def m_W_exp L85
def m_W_exp_sigma L86
def m_Z_exp L89
def m_Z_exp_sigma L90
def m_H_exp L93
def m_H_exp_sigma L94
theorem lepton_params_derived L101
theorem upquark_params_derived L107
theorem downquark_params_derived L113
theorem generation_torsion_derived L120
theorem lepton_rungs_derived L124
def rs_mass_MeV L132
def ratio_mu_e_RS L139
theorem ratio_mu_e_RS_eq L143
def ratio_tau_e_RS L152
theorem ratio_tau_e_RS_eq L156
def ratio_mu_e_exp L162
def ratio_tau_e_exp L165
theorem phi_pow_11_approx L173
theorem phi_pow_17_approx L230
theorem ratio_mu_e_exp_value L320
theorem ratio_tau_e_exp_value L325
theorem raw_prediction_discrepancy L342
def mass_summary L358