`phi_pos`

proved

show as: view math explainer →

module: IndisputableMonolith.Compat.Constants
domain: Compat
line: 17 · github
papers citing: none yet

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.Compat.Constants on GitHub at line 17.

browse module

All declarations in this module, on Recognition.

explainer page

A cached Ask Recognition explainer exists for this declaration.

open explainer

depends on

Constants IndisputableMonolith.CPM.LawOfExistence

formal source

  14
  15abbrev phi : ℝ := IndisputableMonolith.Constants.phi
  16
  17lemma phi_pos : 0 < phi := IndisputableMonolith.Constants.phi_pos
  18
  19/-- Cohesion energy (placeholder) -/
  20def E_coh : ℝ := IndisputableMonolith.Constants.E_coh
  21lemma E_coh_pos : 0 < E_coh := IndisputableMonolith.Constants.E_coh_pos
  22
  23/-- Fundamental tick duration τ₀ (placeholder) -/
  24def tau0 : ℝ := IndisputableMonolith.Constants.tick
  25lemma tau0_pos : 0 < tau0 := by
  26  simpa [tau0] using (zero_lt_one : 0 < (1 : ℝ))
  27
  28/-- Fundamental length ℓ₀ (placeholder) -/
  29def l0 : ℝ := 1
  30lemma l0_pos : 0 < l0 := by
  31  simpa [l0] using (zero_lt_one : 0 < (1 : ℝ))
  32
  33end
  34
  35end Constants
  36
  37namespace RSBridge
  38namespace Fermion
  39
  40def rung : ℕ := 1
  41
  42end Fermion
  43end RSBridge

papers checked against this theorem

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