module module

`IndisputableMonolith.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

used by (7)

From the project-wide theorem graph. These declarations reference this one in their body.

IndisputableMonolith.Physics.ElectronMass module_import
IndisputableMonolith.Physics.ElectronMass.BaselineDerivation module_import
IndisputableMonolith.Physics.ElectronMass.Necessity module_import
IndisputableMonolith.Physics.LeptonGenerations.Defs module_import
IndisputableMonolith.Physics.LeptonGenerations.Necessity module_import
IndisputableMonolith.RRF.Physics.LeptonGenerations.Defs module_import
IndisputableMonolith.RRF.Physics.LeptonGenerations.Necessity module_import

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

def octave_period L68
theorem octave_period_eq L71
def ledger_bilateral_factor L80
def N_sec L83
theorem N_sec_eq L85
def lepton_B L91
theorem lepton_B_eq L94
def electron_baseline_rung L101
def lepton_R0 L107
theorem lepton_R0_eq L110
def coherence_exponent L118
theorem coherence_exponent_eq L120
def E_coh L125
theorem E_coh_eq L128
def electron_rung L135
theorem electron_rung_eq L138
def electron_charge L141
def lepton_yardstick L147
def lepton_yardstick_explicit L151
theorem lepton_yardstick_eq_explicit L155
def electron_structural_mass L161
def electron_structural_ratio L165
def mass_ref_MeV L177
def electron_residue L181
def predicted_electron_mass L185
theorem electron_structural_mass_forced L197
theorem lepton_sector_is_derived L219