`tau0_ne_zero`

proved

show as: view math explainer →

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

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.Constants.Derivation on GitHub at line 48.

browse module

All declarations in this module, on Recognition.

explainer page

A cached Ask Recognition explainer exists for this declaration.

open explainer

depends on

formal source

  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
  65  have hc2 : c_codata ^ 2 ≠ 0 := pow_ne_zero 2 hc
  66  rw [div_pow, sq_sqrt inner_nonneg]
  67  field_simp
  68
  69/-! ## RS Fundamental Length Scale -/
  70
  71def ell0 : ℝ := c_codata * tau0
  72
  73lemma ell0_pos : 0 < ell0 := mul_pos c_codata_pos tau0_pos
  74lemma ell0_ne_zero : ell0 ≠ 0 := ne_of_gt ell0_pos
  75
  76/-! ## RS Unit System Structure -/
  77
  78structure RSUnitSystem where

papers checked against this theorem

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