G_relation_satisfied

formal source

 135  exact mul_pos (mul_pos Real.pi_pos (pow_pos hc 5)) (sq_pos_of_pos hτ)
 136
 137/-- **Theorem**: G_derived tau0 hbar_codata c_codata = G_codata -/
 138theorem G_relation_satisfied :
 139    G_derived tau0 hbar_codata c_codata = G_codata := by
 140  unfold G_derived
 141  rw [tau0_sq_eq]
 142  have hℏ : hbar_codata ≠ 0 := hbar_codata_ne_zero
 143  have hc : c_codata ≠ 0 := c_codata_ne_zero
 144  have hpi : Real.pi ≠ 0 := ne_of_gt Real.pi_pos
 145  have hc5 : c_codata ^ 5 ≠ 0 := pow_ne_zero 5 hc
 146  field_simp
 147
 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