module module high

`IndisputableMonolith.Masses.Verification`

The Verification module assembles experimental mass anchors and RS-derived interval predictions for leptons, quarks, and the proton binding energy. Researchers auditing mass spectra in Recognition Science cite it to compare phi-ladder outputs against PDG references. The module populates these values by importing constants and phi bounds, serving as a reference layer without new derivations.

claimExperimental anchors $m_e$, $m_μ$, $m_τ$ together with RS predictions on the φ-ladder, including the proton binding-energy interval $(969, 970.4)$ MeV.

background

Recognition Science places masses on the φ-ladder via the yardstick scaled by φ to a rung offset, using the time quantum τ₀ = 1 tick as base unit. The Anchor module centralises the parameter-free constants described in the mass manuscripts, while PhiBounds supplies algebraic inequalities such as 2.236² = 4.999696 < 5 < 5.001956 = 2.237² to bound φ = (1 + √5)/2 rigorously.

proof idea

This is a definition module, no proofs. It structures verification data by importing the Constants, Anchor, and PhiBounds modules to populate reference values and interval predictions for downstream scorecards.

why it matters in Recognition Science

This module feeds ChargedLeptonMassScoreCard for lepton rungs with ZOf = 1332, ElectroweakMasses for the Z boson at rung 1, MuRatioScoreCard for the proton-electron ratio, and the quark and top-quark scorecards. It supplies the verification layer that turns mass-manuscript predictions into falsifiable intervals, such as the proton binding-energy range stated in the module documentation.

scope and limits

Does not derive experimental masses from first principles.
Does not claim exact matches beyond the stated intervals.
Does not incorporate future PDG revisions automatically.
Does not cover every particle or resonance sector.

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