module module

`IndisputableMonolith.RRF.Physics.ElectronMass.Defs`

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 (5)

Lean names referenced from this declaration's body.

IndisputableMonolith.Constants module_import
IndisputableMonolith.Constants.AlphaDerivation module_import
IndisputableMonolith.PhiSupport module_import
IndisputableMonolith.Physics.MassTopology module_import
IndisputableMonolith.RSBridge.Anchor module_import

declarations in this module (12)

def lepton_B L24
def lepton_R0 L27
def E_coh L30
def electron_rung L35
def electron_charge L38
def lepton_yardstick L43
def electron_structural_mass L47
def electron_structural_ratio L51
def mass_ref_MeV L58
def electron_residue L62
def predicted_electron_mass L66
theorem electron_structural_mass_forced L78