isClassical
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.
claimA 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 in Recognition Science
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.
scope and limits
- Does not derive the explicit formula for decoherenceTime.
- Does not incorporate temperature or separation parameters.
- Does not prove the quantum-classical dichotomy.
- Does not assign numerical values to Gap-45.
Lean usage
example (env : EnvironmentCoupling) (t : ℝ) (h : decoherenceTime env ≤ t) : isClassical env t := hformal statement (Lean)
145def isClassical (env : EnvironmentCoupling) (measurementTime : ℝ) : Prop :=
proof body
Definition body.
146 decoherenceTime env ≤ measurementTime
147
148/-- Quantum and classical are complementary. -/