def definition def or abbrev

`decoherenceTime`

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

formal statement (Lean)

 113noncomputable def decoherenceTime (coupling N_env : ℝ) (hc : coupling > 0) (hN : N_env > 0) : ℝ :=

Definition body.

 114  1 / (coupling * N_env)
 115
 116/-- **THEOREM**: Macroscopic objects decohere instantly. -/

From the project-wide theorem graph. These declarations reference this one in their body.

decoherence_decreases_with_coupling in IndisputableMonolith.QFT.Decoherence decl_use
decoherence_decreases_with_modes in IndisputableMonolith.QFT.Decoherence decl_use
decoherenceTime in IndisputableMonolith.QFT.Decoherence decl_use
isClassical in IndisputableMonolith.QFT.Decoherence decl_use
isQuantum in IndisputableMonolith.QFT.Decoherence decl_use
predictedQubitDecoherence in IndisputableMonolith.QFT.Decoherence decl_use
quantum_classical_dichotomy in IndisputableMonolith.QFT.Decoherence decl_use
decoherenceTime in IndisputableMonolith.Quantum.PointerStates decl_use

Lean names referenced from this declaration's body.