module module high

`IndisputableMonolith.Masses.Verification`

Verification module supplies RS mass predictions and PDG reference values for leptons, quarks, and proton binding energy. Scorecard modules cite it to compare φ-ladder outputs against experiment. It consists of definitions and interval bounds that import anchor constants and phi bounds to fix the numerical anchors.

claimThe module defines $m_{RS}(rung, Z)$ via the phi-ladder and states the proton binding-energy prediction lies in the interval $(969, 970.4)$ MeV, together with experimental anchors $m_e^{exp}$, $m_μ^{exp}$, $m_τ^{exp}$.

background

The module sits in the Masses domain and imports the RS time quantum τ₀ = 1 tick, the canonical mass constants derived from first principles, and algebraic bounds on φ = (1 + √5)/2 obtained from the inequalities 2.236² < 5 < 2.237². It introduces rs_mass_MeV together with explicit experimental anchors and predicted values for electrons, muons, taus, and the proton binding energy.

proof idea

This is a definition module, no proofs. It assembles imported constants and applies the phi bounds to certify numerical intervals for the listed predictions.

why it matters in Recognition Science

The module supplies the numerical content for downstream scorecards including ChargedLeptonMassScoreCard (lepton masses on rungs 2, 13, 19 with ZOf = 1332), ElectroweakMasses (Z boson at rung 1), MuRatioScoreCard, QuarkScoreCard, QuarkVerification, and TopQuarkMassScoreCard. It realizes the mass predictions from the Anchor derivation chain.

scope and limits

Does not derive the mass formula from the forcing chain.
Does not claim exact experimental matches beyond the stated intervals.
Does not incorporate new PDG data beyond the listed anchors.
Does not address the full T0-T8 chain or RCL.

used by (6)

From the project-wide theorem graph. These declarations reference this one in their body.

IndisputableMonolith.Masses.ChargedLeptonMassScoreCard module_import
IndisputableMonolith.Masses.ElectroweakMasses module_import
IndisputableMonolith.Masses.MuRatioScoreCard module_import
IndisputableMonolith.Masses.QuarkScoreCard module_import
IndisputableMonolith.Masses.QuarkVerification module_import
IndisputableMonolith.Masses.TopQuarkMassScoreCard module_import

depends on (3)

Lean names referenced from this declaration's body.

IndisputableMonolith.Constants module_import
IndisputableMonolith.Masses.Anchor module_import
IndisputableMonolith.Numerics.Interval.PhiBounds module_import

declarations in this module (53)

lemma phi_eq_goldenRatio L31
def m_e_exp L36
def m_mu_exp L37
def m_tau_exp L38
def rs_mass_MeV L42
def electron_pred L48
def muon_pred L49
def tau_pred L50
lemma zpow_sum3 L52
lemma lepton_pred_eq_aux L56
theorem electron_pred_eq L73
theorem muon_pred_eq L76
theorem tau_pred_eq L79
lemma phi59_gt L84
lemma phi59_lt L86
lemma phi70_gt L88
lemma phi70_lt L90
lemma phi76_gt L92
lemma phi76_lt L94
theorem electron_mass_bounds L99
theorem electron_relative_error L110
theorem muon_mass_bounds L121
theorem muon_relative_error L132
theorem tau_mass_bounds L143
theorem tau_relative_error L154
def ratio_mu_e_exp L165
def ratio_tau_e_exp L166
theorem ratio_mu_e_exp_bounds L168
theorem ratio_tau_e_exp_bounds L172
lemma phi11_gt L176
lemma phi11_lt L187
lemma phi17_gt L199
lemma phi17_lt L214
theorem muon_ratio_undershoot L229
theorem tau_ratio_overshoot L233
theorem muon_electron_ratio_error L237
theorem tau_electron_ratio_error L244
structure MassVerificationCert L253
theorem mass_verification_cert_exists L263
def m_p_exp L281
def proton_binding_pred L283
lemma phi43_gt L285
lemma phi43_lt L287
theorem proton_mass_bounds L291
theorem proton_relative_error L308
theorem phi_ladder_verified L325
def up_quark_pred L353
def charm_quark_pred L357
def top_quark_pred L361
theorem quark_preds_pos L365
theorem charm_up_ratio L373
theorem top_charm_ratio L380
theorem top_quark_pred_order L388