module module high

`IndisputableMonolith.Masses.SMVerification`

This module verifies Standard Model fermion masses against the Recognition Science master mass law by defining particle sectors and computing their phi-ladder positions. Particle physicists and foundational theorists would cite it to check consistency between empirical masses and the rung-based formula. The module imports the mass law and structures verification through type definitions and position calculations for electrons, muons, taus, and quarks.

claimApplies the master mass formula $m = y_s · ϕ^{r-8 + g(Z)}$ to Standard Model fermions, where $y_s$ is the sector yardstick, $r$ the rung, and $g(Z)$ the gap function, via definitions of Fermion, fermionSector, fermionRung, fermionCharge, fermionZ, and fermionMass together with explicit position theorems for electron, muon, tauon, up, charm, and top.

background

The module sits in the Masses domain and imports the master mass law, which states that every stable recognition state occupies a rung on the φ-ladder with mass proportional to coherence energy scaled by sector yardstick and rung position. It introduces auxiliary definitions: Fermion as the inductive type for SM fermions, fermionSector to separate leptons and quarks, fermionRung and fermionZ to locate each particle on the ladder, and fermionMass to compute the resulting value. These rest on the upstream mass law's statement that mass follows the phi-ladder scaling derived from the forcing chain.

proof idea

This is a verification module that applies the imported mass law definitions to specific SM particles. It defines the Fermion type and sector/rung/charge/Z accessors, then supplies explicit position theorems such as electron_mass_pos that instantiate the master formula for each particle without additional lemmas.

why it matters in Recognition Science

The module supplies the concrete SM verification layer that connects the abstract mass law to observed particle masses, feeding any higher-level mass spectrum results that depend on these position theorems. It fills the empirical check step for the phi-ladder mass formula derived from T5 J-uniqueness through T8 D=3 in the unified forcing chain.

scope and limits

Does not derive the master mass law itself.
Does not compute numerical mass values beyond rung positions.
Does not address bosons or composite states.
Does not prove stability or decay properties of the listed fermions.

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