`AlphaInvBounds`

definition

show as: view math explainer →

module: IndisputableMonolith.Constants.ExternalAnchors
domain: Constants
line: 133 · github
papers citing: none yet

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.Constants.ExternalAnchors on GitHub at line 133.

browse module

All declarations in this module, on Recognition.

explainer page

A cached Ask Recognition explainer exists for this declaration.

open explainer

used by

alpha_inv_bounds IndisputableMonolith.Constants.ExternalAnchors

formal source

 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
 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² -/

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.