def
definition
e_SI
show as:
view math explainer →
open explainer
Read the cached plain-language explainer.
open lean source
IndisputableMonolith.Constants.ExternalAnchors on GitHub at line 82.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
used by
formal source
79
80/-- **EXTERNAL ANCHOR**: Elementary charge (exact, SI 2019 definition).
81 e = 1.602176634 × 10⁻¹⁹ C -/
82@[simp]
83noncomputable def e_SI : ℝ := 1.602176634e-19
84
85/-- **EXTERNAL ANCHOR**: Boltzmann constant (exact, SI 2019 definition).
86 k_B = 1.380649 × 10⁻²³ J/K -/
87@[simp]
88noncomputable def kB_SI : ℝ := 1.380649e-23
89
90/-- **EXTERNAL ANCHOR**: Avogadro constant (exact, SI 2019 definition).
91 N_A = 6.02214076 × 10²³ mol⁻¹ -/
92@[simp]
93noncomputable def NA_SI : ℝ := 6.02214076e23
94
95/-- **EXTERNAL ANCHOR**: Gravitational constant (CODATA 2022, measured).
96 G = 6.67430(15) × 10⁻¹¹ m³/(kg·s²)
97 Relative uncertainty: 2.2 × 10⁻⁵ -/
98@[simp]
99noncomputable def G_SI : ℝ := 6.67430e-11
100
101/-- **EXTERNAL ANCHOR**: Gravitational constant uncertainty (1σ). -/
102noncomputable def G_SI_uncertainty : ℝ := 0.00015e-11
103
104end CODATAFundamental
105
106/-! ## Fine Structure Constant
107
108**EXTERNAL ANCHOR SECTION**
109
110The electromagnetic coupling constant, dimensionless.
111-/
112