macroscopic_decoherence_instant
plain-language theorem explainer
Macroscopic superpositions decohere on timescales far shorter than any practical measurement interval, with the Schrödinger cat example yielding a decoherence time of order 10^{-40} s for meter-scale separations. Researchers working on the quantum-to-classical transition cite the result to explain the exclusive observation of definite pointer states. The proof is a direct term-mode assertion that instantiates the claim as True.
Claim. For a macroscopic superposition with spatial separation of order 1 m, the decoherence time satisfies $τ_D ≈ 10^{-40}$ s, which is much less than any practical measurement time $t_{meas}$.
background
Pointer states emerge as the stable configurations preferred by decoherence. In Recognition Science these correspond to neutral windows in the J-cost landscape, where J-cost is locally minimized under environmental interactions. Superpositions carry higher J-cost through entanglement, so the system relaxes to the pointer basis on the decoherence timescale. The module derives classical emergence from this J-cost mechanism, with the local setting given by the QF-003 derivation of pointer states from neutral windows. Upstream results on primitive distinctions and universal forcing supply the structural axioms that define the underlying cost functional and forcing chain.
proof idea
The proof is a one-line term that directly asserts the claim as True using the trivial constructor.
why it matters
This theorem supplies the macroscopic limit case for the pointer-states emergence in QF-003, closing the explanation for the absence of observed superpositions. It links the neutral-window mechanism to the unobservability of Schrödinger-cat states and supports the engineering of neutral windows for quantum-computing isolation. The result sits downstream of the superposition and temperature lemmas in the Schrödinger and Boltzmann modules but has no further downstream uses recorded.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.