`phi`

definition

show as: view math explainer →

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

open explainer

Generate a durable explainer page for this declaration.

open lean source

IndisputableMonolith.Compat.Constants on GitHub at line 15.

browse module

All declarations in this module, on Recognition.

explainer page

Tracked in the explainer inventory; generation is lazy so crawlers do not trigger LLM jobs.

open explainer

depends on

Constants IndisputableMonolith.CPM.LawOfExistence

formal source

  12
  13noncomputable section
  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.