def
definition
alpha_inv_bounds
show as:
view math explainer →
open explainer
Read the cached plain-language explainer.
open lean source
IndisputableMonolith.Constants.ExternalAnchors on GitHub at line 139.
browse module
All declarations in this module, on Recognition.
explainer page
Derivations using this theorem
depends on
formal source
136 codata_year : Nat := 2022
137
138/-- **EXTERNAL ANCHOR** -/
139def alpha_inv_bounds : AlphaInvBounds := {}
140
141end FineStructure
142
143/-! ## Particle Masses
144
145**EXTERNAL ANCHOR SECTION**
146
147Dimensionless mass ratios (from PDG 2024 / CODATA 2022).
148-/
149
150section MassRatios
151
152/-- **EXTERNAL ANCHOR**: Electron mass (CODATA 2022).
153 m_e = 9.1093837139(28) × 10⁻³¹ kg
154 m_e = 0.51099895069(16) MeV/c² -/
155@[simp]
156noncomputable def electron_mass_kg : ℝ := 9.1093837139e-31
157
158/-- **EXTERNAL ANCHOR** -/
159@[simp]
160noncomputable def electron_mass_MeV : ℝ := 0.51099895069
161
162/-- **EXTERNAL ANCHOR**: Muon mass (PDG 2024).
163 m_μ = 105.6583755(23) MeV/c² -/
164@[simp]
165noncomputable def muon_mass_MeV : ℝ := 105.6583755
166
167/-- **EXTERNAL ANCHOR**: Proton mass (CODATA 2022).
168 m_p = 938.27208943(29) MeV/c² -/
169@[simp]