def
definition
planck_mass
show as:
view math explainer →
open explainer
Read the cached plain-language explainer.
open lean source
IndisputableMonolith.Constants.Derivation on GitHub at line 152.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
used by
formal source
149
150def planck_length : ℝ := sqrt (hbar_codata * G_codata / c_codata ^ 3)
151def planck_time : ℝ := sqrt (hbar_codata * G_codata / c_codata ^ 5)
152def planck_mass : ℝ := sqrt (hbar_codata * c_codata / G_codata)
153
154lemma planck_length_pos : 0 < planck_length := by
155 unfold planck_length
156 exact sqrt_pos.mpr (div_pos (mul_pos hbar_codata_pos G_codata_pos) (pow_pos c_codata_pos 3))
157
158lemma planck_time_pos : 0 < planck_time := by
159 unfold planck_time
160 exact sqrt_pos.mpr (div_pos (mul_pos hbar_codata_pos G_codata_pos) (pow_pos c_codata_pos 5))
161
162lemma planck_mass_pos : 0 < planck_mass := by
163 unfold planck_mass
164 exact sqrt_pos.mpr (div_pos (mul_pos hbar_codata_pos c_codata_pos) G_codata_pos)
165
166lemma planck_time_inner_nonneg : 0 ≤ hbar_codata * G_codata / c_codata ^ 5 :=
167 le_of_lt (div_pos (mul_pos hbar_codata_pos G_codata_pos) (pow_pos c_codata_pos 5))
168
169/-- **Theorem**: τ₀ = t_P / √π
170
171This relation shows τ₀ is the Planck time divided by √π. -/
172theorem tau0_planck_relation : tau0 = planck_time / sqrt Real.pi := by
173 unfold tau0 planck_time
174 have hc : c_codata ≠ 0 := c_codata_ne_zero
175 have hpi : Real.pi ≠ 0 := ne_of_gt Real.pi_pos
176 have hpi_pos : 0 < Real.pi := Real.pi_pos
177 have hc_pos : 0 < c_codata := c_codata_pos
178 have hinner_pos : 0 < hbar_codata * G_codata := mul_pos hbar_codata_pos G_codata_pos
179 have hsqrt_pi_pos : 0 < sqrt Real.pi := sqrt_pos.mpr hpi_pos
180 have hsqrt_pi_ne : sqrt Real.pi ≠ 0 := ne_of_gt hsqrt_pi_pos
181 have hc3_pos : 0 < c_codata ^ 3 := pow_pos hc_pos 3
182 have hc5_pos : 0 < c_codata ^ 5 := pow_pos hc_pos 5