module module

`IndisputableMonolith.Physics.ElectronMass.BaselineDerivation`

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

Lean names referenced from this declaration's body.

IndisputableMonolith.Constants module_import
IndisputableMonolith.Constants.AlphaDerivation module_import
IndisputableMonolith.Physics.ElectronMass.Defs module_import

declarations in this module (5)

def lepton_baseline L30
theorem lepton_baseline_eq L32
theorem baseline_matches_electron_rung L36
theorem active_edges_eq_one L41
theorem electron_rung_derived L44