isQuantum
plain-language theorem explainer
The definition marks a system as quantum when its decoherence time exceeds the supplied measurement interval. Researchers deriving first-principles decoherence from discrete structure would cite it to separate coherent from classical regimes. It is realized as a direct inequality on the decoherenceTime function that incorporates mode count and coupling strength.
Claim. A system with environmental coupling $env$ (recording mode count $N$ and strength $g$) is quantum at measurement time $t$ precisely when its decoherence time satisfies $τ_{decoherence}(env) > t$.
background
The module QF-009 derives decoherence timescales from the Gap-45 threshold, the ratio ≈10^45 between Planck and biological scales that separates preserved coherence from environmental entanglement. EnvironmentCoupling is the structure holding the number of modes and a coupling strength in [0,1]; decoherenceTime is defined from these via τ_decoherence ≈ τ_0 × φ^(-N×g). Upstream, the active-edge count A from IntegrationGap supplies the fundamental tick, while TimeEmergence.before supplies the ordering used in temporal comparisons.
proof idea
One-line definition that equates the quantum property directly to the strict inequality decoherenceTime env > measurementTime.
why it matters
This definition supplies the quantum disjunct for the downstream theorem quantum_classical_dichotomy. It operationalizes the Gap-45 mechanism stated in the module documentation and links to the phi-ladder scaling that appears throughout the Recognition framework. No open scaffolding questions are attached to this declaration.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.