decoherence_decreases_with_modes
plain-language theorem explainer
Decoherence time decreases when the number of environmental modes increases at fixed positive coupling strength. Researchers bounding coherence lifetimes in discrete-structure models of quantum-to-classical transitions would cite this. The proof unfolds the decoherenceTime definition, rewrites the common strength factor, and reduces the claim to a strict exponent inequality that follows from phi greater than one via Real.rpow_lt_rpow_of_exponent_lt.
Claim. Let $env_1, env_2$ be environment couplings (structures recording natural-number modes $N$ and real strength $g$ with $0 < g < 1$) such that $N_1 < N_2$ and $g_1 = g_2 > 0$. Then the decoherence time satisfies $τ_0 φ^{-N_2 g} < τ_0 φ^{-N_1 g}$, where $τ_0 ≈ 7.3 × 10^{-15}$ s is the reference recognition tick and $φ$ is the golden ratio.
background
The QFT.Decoherence module derives decoherence timescales from the Gap-45 threshold (ratio ≈10^45 between Planck and biological scales). Quantum coherence holds below this threshold; above it the system entangles with the environment and decoheres. EnvironmentCoupling records the number of modes $N$ and coupling strength $g ∈ [0,1]$. Decoherence time is defined by $τ_{decoherence}(env) = τ_0 × φ^{-N g}$, with $τ_0$ taken from tau0_seconds in GravityBridge and $φ$ from Constants satisfying $φ > 1.5$.
proof idea
The tactic proof unfolds decoherenceTime and tau0_seconds, rewrites using equal strengths, and applies mul_lt_mul_of_pos_left with the positive constant 7.3e-15. It obtains $φ > 1$ from phi_gt_onePointFive via linarith, establishes the exponent inequality via Nat.cast_lt and nlinarith, then concludes with Real.rpow_lt_rpow_of_exponent_lt.
why it matters
The result supplies the quantitative dependence of decoherence time on mode count inside the Gap-45 framework, confirming that stronger environmental coupling drives faster loss of coherence. It directly supports the module's claim that decoherence occurs once interaction exceeds the 10^45 threshold and supplies the scaling needed for error-correction proposals based on the discrete recognition structure. No downstream theorems are recorded yet.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.