def
definition
alpha_inv_CODATA
show as:
view math explainer →
open explainer
Read the cached plain-language explainer.
open lean source
IndisputableMonolith.Constants.ExternalAnchors on GitHub at line 126.
browse module
All declarations in this module, on Recognition.
explainer page
Derivations using this theorem
used by
formal source
123
124/-- **EXTERNAL ANCHOR**: Inverse fine structure constant (CODATA 2022).
125 α⁻¹ = 137.035999177(21) -/
126@[simp]
127noncomputable def alpha_inv_CODATA : ℝ := 137.035999177
128
129/-- **EXTERNAL ANCHOR**: α⁻¹ uncertainty (1σ). -/
130noncomputable def alpha_inv_CODATA_uncertainty : ℝ := 0.000000021
131
132/-- **EXTERNAL ANCHOR**: α⁻¹ empirical bounds (±3σ). -/
133structure AlphaInvBounds where
134 lower : ℝ := 137.035999114 -- -3σ
135 upper : ℝ := 137.035999240 -- +3σ
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