lemma
proved
planck_time_pos
show as:
view math explainer →
open explainer
Read the cached plain-language explainer.
open lean source
IndisputableMonolith.Constants.Derivation on GitHub at line 158.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
formal source
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
183 have hinner5_nonneg : 0 ≤ hbar_codata * G_codata / c_codata ^ 5 :=
184 le_of_lt (div_pos hinner_pos hc5_pos)
185 have hc3 : c_codata ^ 3 ≠ 0 := pow_ne_zero 3 hc
186 have hc5 : c_codata ^ 5 ≠ 0 := pow_ne_zero 5 hc
187 have hinner3_div_pos : 0 < hbar_codata * G_codata / (Real.pi * c_codata ^ 3) :=
188 div_pos hinner_pos (mul_pos hpi_pos hc3_pos)