`critical_modes_specification`

proved

show as: view math explainer →

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

open explainer

Generate a durable explainer page for this declaration.

open lean source

IndisputableMonolith.QFT.Decoherence on GitHub at line 167.

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

formal source

 164/-- The critical modes formula inverts the decoherence formula.
 165    Proof outline: If N = -ln(t/τ₀)/(g·ln(φ)), then:
 166    τ₀ · φ^(-N·g) = τ₀ · φ^(ln(t/τ₀)/ln(φ)) = τ₀ · (t/τ₀) = t -/
 167theorem critical_modes_specification :
 168    ∀ (t g : ℝ), t > 0 → g > 0 →
 169    criticalModes t g = -Real.log (t / tau0_seconds) / (g * Real.log phi) := by
 170  intro t g ht hg
 171  unfold criticalModes
 172  simp [ht, hg]
 173
 174/-! ## Qubit Decoherence Examples -/
 175
 176/-- Typical superconducting qubit parameters. -/
 177structure QubitParams where
 178  /-- T1 relaxation time (seconds). -/
 179  t1 : ℝ
 180  /-- T2 dephasing time (seconds). -/
 181  t2 : ℝ
 182  /-- Operating temperature (Kelvin). -/
 183  temperature : ℝ
 184  /-- Number of coupled modes. -/
 185  env_modes : ℕ
 186
 187/-- Typical superconducting qubit. -/
 188def typicalSCQubit : QubitParams := {
 189  t1 := 50e-6,        -- 50 μs
 190  t2 := 70e-6,        -- 70 μs
 191  temperature := 0.015,-- 15 mK
 192  env_modes := 10     -- Estimated
 193}
 194
 195/-- Predicted decoherence time for the typical qubit. -/
 196noncomputable def predictedQubitDecoherence : ℝ :=
 197  decoherenceTime ⟨typicalSCQubit.env_modes, 0.5, by norm_num, by norm_num⟩

papers checked against this theorem

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