def
definition
alpha_CODATA
show as:
view math explainer →
open explainer
Read the cached plain-language explainer.
open lean source
IndisputableMonolith.Constants.ExternalAnchors on GitHub at line 118.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
formal source
115/-- **EXTERNAL ANCHOR**: Fine structure constant (CODATA 2022).
116 α = 7.2973525643(11) × 10⁻³
117 Relative uncertainty: 1.5 × 10⁻¹⁰ -/
118@[simp]
119noncomputable def alpha_CODATA : ℝ := 7.2973525643e-3
120
121/-- **EXTERNAL ANCHOR**: Fine structure constant uncertainty (1σ). -/
122noncomputable def alpha_CODATA_uncertainty : ℝ := 0.0000000011e-3
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-/