isClassical
plain-language theorem explainer
A system with given environment coupling is classical when its decoherence time is at most the measurement time. Researchers analyzing the quantum-to-classical transition cite this definition to mark the regime boundary. It is a direct one-line definition that invokes the decoherenceTime function and performs the comparison.
Claim. A system with environment coupling $E$ (number of modes $N$, strength $g$) is classical at measurement time $t$ if the decoherence time satisfies $τ_D(E) ≤ t$, where $τ_D(E) = τ_0 φ^{-N g}$.
background
The QFT.Decoherence module derives decoherence timescales from the Gap-45 threshold, where coherence is preserved below the threshold and entanglement with the environment produces decoherence above it. EnvironmentCoupling is the structure that records the number of environmental modes and the coupling strength (bounded by 0 ≤ strength ≤ 1). The upstream decoherenceTime definition computes τ_decoherence = τ_0 × φ^(-N × g) using the fundamental coherence time τ_0. The module states that Gap-45 separates quantum information preservation from classical information sharing.
proof idea
One-line definition that applies decoherenceTime to the supplied environment and checks the inequality against the measurement time.
why it matters
This definition supplies the classical case for the downstream quantum_classical_dichotomy theorem, which proves that for any environment and time the system satisfies isQuantum or isClassical. It completes the Gap-45 mechanism in the QF-009 target, linking decoherence to the point where information is shared with the environment. It leaves open the experimental calibration of the precise Gap-45 numerical value.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.