decoherence_decreases_with_coupling
plain-language theorem explainer
Stronger environmental coupling shortens decoherence time via the explicit scaling τ_decoherence = τ₀ φ^{-N g}. Researchers modeling quantum-classical transitions from the Gap-45 threshold would cite the monotonicity result when bounding coherence lifetimes. The proof unfolds the formula, reduces the comparison to an exponent inequality using φ > 1, and invokes real-power monotonicity after applying mul_lt_mul_of_pos_left.
Claim. Let env1 and env2 be environment couplings sharing the same positive mode count N. If the coupling strength satisfies g₁ < g₂, then τ_decoherence(env2) < τ_decoherence(env1), where τ_decoherence(g) := τ₀ ⋅ φ^{-N g} with τ₀ the reference tick and φ the golden ratio.
background
The module derives decoherence timescales from the Gap-45 threshold separating quantum coherence (information preserved below threshold) from classical entanglement (information shared above threshold). EnvironmentCoupling is the structure bundling modes N : ℕ and strength g : ℝ with 0 ≤ g ≤ 1. The decoherence time is defined by the formula τ_decoherence = τ₀ × φ^{-N g}, where τ₀ comes from tau0_seconds ≈ 7.3 × 10^{-15} s and φ is the golden ratio.
proof idea
The tactic proof unfolds decoherenceTime, tau0_seconds and phi. It obtains positivity of τ₀ by norm_num, rewrites via the modes equality, then applies mul_lt_mul_of_pos_left. It derives φ > 1 from Constants.phi_gt_onePointFive via linarith, establishes the exponent inequality -(N g₂) < -(N g₁) by nlinarith on the strength hypothesis, and finishes with Real.rpow_lt_rpow_of_exponent_lt.
why it matters
The result fills the monotonicity step needed for the quantum-versus-classical regime section of QF-009. It relies on the phi scaling from the forcing chain (T5 J-uniqueness and T6 fixed point) and the eight-tick octave that sets τ₀. No downstream uses appear in the graph, yet the declaration directly supports the Gap-45 patent proposals for error correction and qubit design.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.