def
definition
planck_time
show as:
view math explainer →
open explainer
Read the cached plain-language explainer.
open lean source
IndisputableMonolith.Constants.Derivation on GitHub at line 151.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
used by
formal source
148/-! ## Planck Units -/
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