`c_codata`

definition

show as: view math explainer →

module: IndisputableMonolith.Constants.Derivation
domain: Constants
line: 24 · github
papers citing: none yet

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.Constants.Derivation on GitHub at line 24.

browse module

All declarations in this module, on Recognition.

explainer page

A cached Ask Recognition explainer exists for this declaration.

open explainer

used by

formal source

  21
  22/-! ## CODATA Reference Values -/
  23
  24def c_codata : ℝ := 299792458
  25def hbar_codata : ℝ := 1.054571817e-34
  26def G_codata : ℝ := 6.67430e-11
  27
  28lemma c_codata_pos : 0 < c_codata := by unfold c_codata; norm_num
  29lemma hbar_codata_pos : 0 < hbar_codata := by unfold hbar_codata; norm_num
  30lemma G_codata_pos : 0 < G_codata := by unfold G_codata; norm_num
  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) :=

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.