c_derived_eq_codata

formal source

  97
  98def c_derived (u : RSUnitSystem) : ℝ := u.ℓ / u.τ
  99
 100theorem c_derived_eq_codata (u : RSUnitSystem) : c_derived u = c_codata := by
 101  unfold c_derived
 102  have h := u.consistency
 103  have hτ : u.τ ≠ 0 := ne_of_gt u.τ_pos
 104  field_simp at h ⊢
 105  linarith
 106
 107lemma c_derived_pos (u : RSUnitSystem) : 0 < c_derived u := by
 108  rw [c_derived_eq_codata]; exact c_codata_pos
 109
 110def hbar_derived (τ G_val c_val : ℝ) : ℝ := Real.pi * c_val ^ 5 * τ ^ 2 / G_val
 111
 112lemma hbar_derived_pos (τ G_val c_val : ℝ) (hτ : 0 < τ) (hG : 0 < G_val) (hc : 0 < c_val) :
 113    0 < hbar_derived τ G_val c_val := by
 114  unfold hbar_derived
 115  apply div_pos _ hG
 116  exact mul_pos (mul_pos Real.pi_pos (pow_pos hc 5)) (sq_pos_of_pos hτ)
 117
 118/-- **Theorem**: hbar_derived tau0 G_codata c_codata = hbar_codata -/
 119theorem planck_relation_satisfied :
 120    hbar_derived tau0 G_codata c_codata = hbar_codata := by
 121  unfold hbar_derived
 122  rw [tau0_sq_eq]
 123  have hG : G_codata ≠ 0 := G_codata_ne_zero
 124  have hc : c_codata ≠ 0 := c_codata_ne_zero
 125  have hpi : Real.pi ≠ 0 := ne_of_gt Real.pi_pos
 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