decoherenceTime
plain-language theorem explainer
DecoherenceTime supplies the explicit timescale for loss of quantum coherence as the reciprocal of coupling strength times environmental mode count. Researchers modeling the quantum-to-classical transition cite it to obtain order-of-magnitude estimates for macroscopic systems where N_env reaches 10^23. The definition is a direct algebraic expression implementing the inverse rate that follows from many-body J-cost minimization.
Claim. The decoherence time for a system with positive coupling strength $g$ and positive environment size $N$ is given by $1/(g N)$.
background
Recognition Science derives classical emergence from many-body J-cost minimization under the Recognition Composition Law. Single-particle superpositions carry low J-cost while correlated states across N particles scale quadratically or worse, so the environment functions as a regulator that selects low-cost product states. The module QF-011 formalizes this mechanism and supplies the concrete timescale that converts the abstract cost scaling into a measurable rate.
proof idea
The definition is a one-line algebraic expression that directly implements the inverse product of the two positive parameters.
why it matters
This definition anchors the downstream theorems in QFT.Decoherence that establish decoherence decreases with coupling and with modes, together with the predicates isClassical and isQuantum. It realizes the QF-011 claim that macroscopic objects decohere on timescales around 10^{-23} s, closing the step from the J-cost composition law to observable pointer-state selection. The scaling supplies the concrete rate that connects to the phi-ladder through the exponential forms appearing in the upstream QFT and PointerStates definitions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.