module module moderate

`IndisputableMonolith.Verification.MassComparison`

Verification module that records PDG-style experimental rest masses and one-sigma uncertainties for the charged leptons and light quarks. Downstream mass-ladder checks cite these constants when comparing Recognition Science predictions to data. The file is pure data definitions; no theorems are proved here.

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

background

Recognition Science places particle masses on a $\varphi$-ladder: a yardstick times $\varphi^{r_{\mathrm{ung}}-8+\mathrm{gap}(Z)}$. The Model-layer module Masses.Anchor centralises the parameter-free derived constants; nothing there claims experimental agreement. This Verification module supplies the complementary experimental side.

It imports RS constants ($\tau_0=1$ tick), rigorous interval bounds on $\varphi=(1+\sqrt{5})/2$, and the T10 lepton-generation definitions that separate mass-ladder data from theorems. The sibling constants are the usual PDG central values and sigmas (electron example: $0.51099895069(16)$ MeV), stored as plain Real literals for residual and band comparisons.

proof idea

This is a definition module, no proofs. It declares experimental mass and uncertainty constants for $e,\mu,\tau$ and $u,d,s$ as concrete real values. Structure is data-only: named m_*_exp / m_*_exp_sigma bindings with no tactic or term proofs.

why it matters in Recognition Science

Closes the data half of the mass-comparison loop against the first-principles ladder in Masses.Anchor and the T10 lepton-generation defs. Without fixed experimental anchors, residual theorems cannot state numerical agreement bands. No downstream edges are recorded yet in the graph; the intended consumers are verification lemmas that bound $|m_{\mathrm{RS}}-m^{\mathrm{exp}}|/\sigma$. Ties to the primer mass formula (yardstick $\times\varphi^{r-8+\mathrm{gap}(Z)}$) and to $\varphi$ bounds used when converting ladder exponents into MeV.

scope and limits

Does not derive or prove any RS mass prediction.
Does not claim experimental agreement; only stores PDG-style inputs.
Does not cover heavy quarks, neutrinos, or bosons.
Does not update values when PDG revisions appear; literals are frozen.
Does not encode unit conversions beyond the stated MeV convention.

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