module module

`IndisputableMonolith.Masses.SMVerification`

show as: view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

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