module module moderate

`IndisputableMonolith.Masses.SMVerification`

This module verifies Standard Model fermion masses by applying the Recognition Science master mass law to explicit particle definitions. Particle physicists checking consistency between observed masses and the phi-ladder would reference it. The module consists of type definitions for fermions together with concrete rung and mass calculations for the electron, muon, tau, and selected quarks.

claimFermion types with sector, rung, charge, and Z assignments; masses given by $m = y \cdot \phi^{r-8+g(Z)}$ where $y$ is the sector yardstick, $r$ the rung, and $g(Z)$ the gap function, for the electron, muon, tauon, up, charm, and top.

background

The module imports the Master Mass Law, whose doc-comment states that every stable recognition state occupies a rung on the φ-ladder and that mass is proportional to coherence energy scaled by sector yardstick and rung position. It introduces sibling definitions Fermion, fermionSector, fermionRung, fermionCharge, fermionZ, and fermionMass that specialize the general law to the Standard Model. These sit inside the Masses domain and rely on the phi-ladder structure supplied by the upstream MassLaw module.

proof idea

this is a definition module, no proofs

why it matters in Recognition Science

The module supplies the concrete SM fermion instances required by the Recognition Science mass framework. It connects the abstract mass law (from the imported MassLaw module) to the six fermions whose masses are computed via the phi-ladder formula. No downstream declarations are listed, indicating the verification stands as a terminal check within the Masses domain.

scope and limits

Does not derive masses for bosons or beyond-Standard-Model states.
Does not prove numerical agreement with experimental values beyond the listed fermions.
Does not address the full forcing chain or Recognition Composition Law.
Does not contain any theorem statements or sorry placeholders.

depends on (1)

Lean names referenced from this declaration's body.

IndisputableMonolith.Masses.MassLaw module_import

declarations in this module (27)

inductive Fermion L35
def fermionSector L41
def fermionRung L46
def fermionCharge L57
def fermionZ L62
def fermionMass L64
theorem electron_mass_pos L69
theorem muon_mass_pos L72
theorem tauon_mass_pos L75
theorem up_mass_pos L78
theorem charm_mass_pos L81
theorem top_mass_pos L84
theorem down_mass_pos L87
theorem strange_mass_pos L90
theorem bottom_mass_pos L93
theorem all_fermion_masses_pos L96
theorem muon_rung_minus_electron_rung L101
theorem tauon_rung_minus_electron_rung L107
def pdg_electron_MeV L144
def pdg_muon_MeV L145
def pdg_tauon_MeV L146
def pdg_mu_e_ratio L148
theorem pdg_mu_e_ratio_approx L150
theorem fermion_count L156
theorem charged_fermion_generations L158
structure SMVerificationCert L162
def sm_verification_cert L168