module module moderate

`IndisputableMonolith.Masses.Verification`

Verification layer for Recognition Science mass predictions: experimental lepton anchors, RS MeV conversions, and closed equalities for electron, muon, and tau on the phi-ladder. Mass-sector auditors cite it when checking that predicted rung formulas reduce to explicit powers of phi. The module mixes parameter-free definitions with short algebraic identities and interval facts; one recorded claim is the proton binding-energy band (969, 970.4) MeV.

claimCollects RS mass predictions in MeV via the phi-ladder formula, experimental lepton masses $m_e$, $m_\mu$, $m_\tau$, predicted values $\mathrm{electron\_pred}$, $\mathrm{muon\_pred}$, $\mathrm{tau\_pred}$, and equalities identifying those predictions with explicit $\phi$-power expressions; records that the proton binding-energy prediction lies in $(969, 970.4)$ MeV.

background

Recognition Science places particle masses on a discrete phi-ladder: mass equals a fixed yardstick times $\phi^{\mathrm{rung}-8+\mathrm{gap}(Z)}$, with $\phi$ the golden ratio forced as the self-similar fixed point (T6). This module sits in the Masses domain and imports the canonical, parameter-free anchors from Masses.Anchor (Model-layer constants only; no experimental-agreement theorems), fundamental RS units from Constants, and rigorous algebraic bounds on $\phi=(1+\sqrt{5})/2$ from PhiBounds.

Sibling content defines experimental lepton masses, the RS-to-MeV conversion, and the three charged-lepton predictions, then proves they match explicit power sums in $\phi$. The module doc flags a proton binding-energy interval claim in $(969, 970.4)$ MeV as part of the same verification surface.

proof idea

Not a single theorem: a verification module. Definitions fix experimental anchors ($m_e$, $m_\mu$, $m_\tau$), the MeV conversion rs_mass_MeV, and the three lepton predictions. Equality lemmas (lepton_pred_eq_aux, electron_pred_eq, muon_pred_eq, and the power-sum helper zpow_sum3) reduce each prediction to an explicit combination of powers of $\phi$, using phi_eq_goldenRatio and the interval machinery from PhiBounds. Interval or numeric claims (including the proton binding band in the module doc) are discharged by those algebraic bounds rather than by floating-point search.

why it matters in Recognition Science

Supplies the checked lepton-side mass surface that the electroweak sector builds on. Downstream, Masses.ElectroweakMasses imports this module and predicts boson masses by the same rung mechanism (e.g. $m_Z=2\cdot\phi^{51}/10^6$ MeV at electroweak rung 1). Without the closed lepton equalities and the shared MeV conversion, those boson formulas would float free of the charged-lepton ladder. In the broader framework this is the mass-formula checkpoint on the phi-ladder (yardstick $\cdot\phi^{\mathrm{rung}-8+\mathrm{gap}(Z)}$), tying Model-layer anchors to the constants fixed by T5–T6 and the RCL.

scope and limits

Does not prove experimental agreement; Anchor constants stay in the Model layer.
Does not derive the mass yardstick or gap function; those are imported.
Does not treat quark or hadron spectra beyond the cited proton binding interval.
Does not prove electroweak boson masses; that lives in the downstream module.
Does not replace PhiBounds; numeric intervals rely on that import.

used by (1)

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

IndisputableMonolith.Masses.ElectroweakMasses 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 L262
theorem mass_verification_cert_exists L272
def m_p_exp L290
def proton_binding_pred L292
lemma phi43_gt L294
lemma phi43_lt L296
theorem proton_mass_bounds L300
theorem proton_relative_error L317
theorem phi_ladder_verified L336
def up_quark_pred L364
def charm_quark_pred L368
def top_quark_pred L372
theorem quark_preds_pos L376
theorem charm_up_ratio L384
theorem top_charm_ratio L391
theorem top_quark_pred_order L399