G_codata_ne_zero

formal source

  31
  32lemma c_codata_ne_zero : c_codata ≠ 0 := ne_of_gt c_codata_pos
  33lemma hbar_codata_ne_zero : hbar_codata ≠ 0 := ne_of_gt hbar_codata_pos
  34lemma G_codata_ne_zero : G_codata ≠ 0 := ne_of_gt G_codata_pos
  35
  36/-! ## RS Fundamental Time Quantum -/
  37
  38def tau0 : ℝ := sqrt (hbar_codata * G_codata / (Real.pi * c_codata ^ 3)) / c_codata
  39
  40lemma tau0_pos : 0 < tau0 := by
  41  unfold tau0
  42  apply div_pos
  43  · apply sqrt_pos.mpr
  44    apply div_pos (mul_pos hbar_codata_pos G_codata_pos)
  45    exact mul_pos Real.pi_pos (pow_pos c_codata_pos 3)
  46  · exact c_codata_pos
  47
  48lemma tau0_ne_zero : tau0 ≠ 0 := ne_of_gt tau0_pos
  49
  50lemma inner_pos : 0 < hbar_codata * G_codata / (Real.pi * c_codata ^ 3) := by
  51  apply div_pos (mul_pos hbar_codata_pos G_codata_pos)
  52  exact mul_pos Real.pi_pos (pow_pos c_codata_pos 3)
  53
  54lemma inner_nonneg : 0 ≤ hbar_codata * G_codata / (Real.pi * c_codata ^ 3) :=
  55  le_of_lt inner_pos
  56
  57/-- **Key Lemma**: τ₀² = ℏG/(πc⁵) -/
  58theorem tau0_sq_eq : tau0 ^ 2 = hbar_codata * G_codata / (Real.pi * c_codata ^ 5) := by
  59  unfold tau0
  60  have hc : c_codata ≠ 0 := c_codata_ne_zero
  61  have hpi : Real.pi ≠ 0 := ne_of_gt Real.pi_pos
  62  have hc3 : c_codata ^ 3 ≠ 0 := pow_ne_zero 3 hc
  63  have hc5 : c_codata ^ 5 ≠ 0 := pow_ne_zero 5 hc
  64  have hdenom1 : Real.pi * c_codata ^ 3 ≠ 0 := mul_ne_zero hpi hc3