decoherenceTime
The definition supplies the decoherence timescale for a quantum system coupled to an environment with N modes and strength g. Researchers working on quantum-to-classical transitions would cite it when deriving pointer states or error rates in qubits. It is a direct algebraic expression using the reference tick and golden-ratio scaling. The expression follows immediately from the module formula without additional lemmas.
claimThe decoherence time is given by $τ = τ_0 φ^{-N g}$ where $N$ is the number of environmental modes and $g$ the coupling strength in $(0,1]$.
background
EnvironmentCoupling is the structure holding the number of modes (a natural number) and the coupling strength (a real in [0,1]). tau0_seconds supplies the reference recognition tick in seconds, defined as approximately 7.3 × 10^{-15} s from the RS constants. phi is the golden ratio used for scaling throughout the framework. The module sets the local context as QF-009, deriving decoherence timescales from the Gap-45 threshold that separates the quantum regime (coherent superposition below the threshold) from the classical regime (entanglement with the environment above it). Upstream results include the modes definition from Galerkin2D and the tau0_seconds alias in the same module.
proof idea
One-line definition that multiplies tau0_seconds by phi raised to the negative product of the modes count and the strength value. It directly unfolds the formula τ_decoherence = τ_0 × φ^(-N × g) using the referenced tau0_seconds and phi constants.
why it matters in Recognition Science
This definition feeds the theorems decoherence_decreases_with_modes, decoherence_decreases_with_coupling, isQuantum, isClassical, and quantum_classical_dichotomy. It implements the Gap-45 mechanism from the module documentation, where decoherence occurs once interaction exceeds roughly 10^45 operations per characteristic time. The construction supports the paper claim of first-principles decoherence from discrete structure and supplies the concrete timescale used in predictedQubitDecoherence.
scope and limits
- Does not derive the numerical value of Gap-45 from the forcing chain.
- Does not count physical modes for a concrete apparatus.
- Does not incorporate temperature or separation distance into the timescale.
- Does not address relativistic corrections to the reference tick.
Lean usage
decoherenceTime ⟨10, 0.5, by norm_num, by norm_num⟩formal statement (Lean)
93noncomputable def decoherenceTime (env : EnvironmentCoupling) : ℝ :=
proof body
Definition body.
94 tau0_seconds * Real.rpow phi (-(env.modes : ℝ) * env.strength)
95
96/-- **THEOREM**: Decoherence time decreases with more environmental modes. -/