G_derived

formal source

 126  have hc5 : c_codata ^ 5 ≠ 0 := pow_ne_zero 5 hc
 127  field_simp
 128
 129def G_derived (τ hbar_val c_val : ℝ) : ℝ := Real.pi * c_val ^ 5 * τ ^ 2 / hbar_val
 130
 131lemma G_derived_pos (τ hbar_val c_val : ℝ) (hτ : 0 < τ) (hℏ : 0 < hbar_val) (hc : 0 < c_val) :
 132    0 < G_derived τ hbar_val c_val := by
 133  unfold G_derived
 134  apply div_pos _ hℏ
 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