`tau0_seconds`

definition

show as: view math explainer →

module: IndisputableMonolith.QFT.Decoherence
domain: QFT
line: 55 · github
papers citing: none yet

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.QFT.Decoherence on GitHub at line 55.

browse module

All declarations in this module, on Recognition.

explainer page

A cached Ask Recognition explainer exists for this declaration.

open explainer

depends on

used by

formal source

  52/-! ## Gap-45 Constants -/
  53
  54/-- Reference tick τ₀ in seconds. -/
  55noncomputable def tau0_seconds : ℝ := 7.3e-15
  56
  57/-- Golden ratio (local alias for Constants.phi). -/
  58noncomputable def phi : ℝ := Constants.phi
  59
  60/-- The Gap-45 threshold (approximate). -/
  61noncomputable def gap45 : ℝ := 10^45
  62
  63/-- Planck time in seconds. -/
  64noncomputable def tau_planck : ℝ := 5.4e-44
  65
  66/-- Biological/classical timescale in seconds. -/
  67noncomputable def tau_bio : ℝ := 1.0
  68
  69/-- The logarithmic gap between biological and Planck timescales.
  70    log₁₀(tau_bio / tau_planck) ≈ log₁₀(1 / 5.4e-44) ≈ 43.3
  71
  72    We prove this is approximately 43-44 orders of magnitude. -/
  73def timescale_gap_log10 : ℚ := 43  -- Approximate value
  74
  75/-- **THEOREM**: The gap is between 43 and 45 orders of magnitude. -/
  76theorem gap_range : 43 ≤ timescale_gap_log10 ∧ timescale_gap_log10 < 45 := by
  77  unfold timescale_gap_log10
  78  constructor <;> norm_num
  79
  80/-! ## Decoherence Time Formula -/
  81
  82/-- The number of environmental modes coupled to the system. -/
  83structure EnvironmentCoupling where
  84  /-- Number of modes. -/
  85  modes : ℕ

papers checked against this theorem

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