module module moderate

`IndisputableMonolith.Masses.SMVerification`

This module applies the master mass law to Standard Model fermions by assigning each particle a sector, rung, charge, and Z value on the φ-ladder. It supplies concrete definitions for the electron, muon, tau, up, charm, and top that map directly onto the coherence-energy scaling. Researchers modeling mass hierarchies or testing Recognition Science predictions against collider data would cite these assignments. The module is built entirely from definitions that instantiate the abstract mass formula for the six fermions.

claimThe module supplies the assignments fermionSector(f), fermionRung(f), fermionCharge(f), fermionZ(f) and the resulting fermionMass(f) = y \cdot \phi^{r-8+g(Z)} for each Standard Model fermion f, where y is the sector yardstick, r the rung index, and g(Z) the gap function.

background

The module imports the Master Mass Law, which states that every stable recognition state occupies a rung on the φ-ladder and that mass is proportional to coherence energy E_coh scaled by sector yardstick and rung position. It therefore inherits the φ-ladder structure and the yardstick scaling already formalized in MassLaw. The local setting is the Masses domain, where the general mass formula is specialized to the six fermions of the Standard Model via explicit rung and sector data.

proof idea

This is a definition module, no proofs. It consists of type and function definitions (Fermion, fermionSector, fermionRung, fermionCharge, fermionZ, fermionMass) together with the six concrete mass_pos lemmas that record the rung assignments for each fermion.

why it matters in Recognition Science

The module supplies the concrete SM instances required by the master mass law, thereby linking the abstract φ-ladder construction to the observed fermion spectrum. It sits directly downstream of the MassLaw module and provides the data that any later verification of mass ratios or coupling constants would invoke.

scope and limits

Does not derive the φ-ladder or the master mass formula.
Does not treat gauge bosons or the Higgs sector.
Does not compute numerical mass values, only rung positions.
Does not address mixing angles or CP phases.

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