IndisputableMonolith.Compat.Constants

   1import Mathlib.Analysis.SpecialFunctions.Sqrt
   2import Mathlib.Data.Real.Basic
   3import IndisputableMonolith.Constants
   4
   5/-!
   6Project-wide constants and minimal structural lemmas.
   7-/
   8
   9namespace Constants
  10
  11open IndisputableMonolith.Constants
  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
  44