quantum_classical_dichotomy
plain-language theorem explainer
The theorem states that for any environment coupling and real time t, the system is either quantum or classical according to whether t lies before or after the decoherence time. Researchers in quantum foundations or decoherence modeling would cite it as the formal dichotomy arising from the Gap-45 threshold in Recognition Science. The proof is a one-line term proof that unfolds the two predicates and applies the trichotomy law on the reals.
Claim. For every environment coupling $env$ and time $t ∈ ℝ$, either the system is quantum ($t < τ_{decoherence}(env)$) or classical ($t ≥ τ_{decoherence}(env)$).
background
The QFT.Decoherence module derives decoherence timescales from the Gap-45 threshold, defined as the ratio separating Planck-scale ticks from biological timescales. Quantum coherence persists below this threshold; above it the system entangles with the environment. The EnvironmentCoupling structure supplies the number of modes and a coupling strength in [0,1], which enter the formula τ_decoherence ≈ τ_0 × φ^(-N·g). Upstream results include the convex J-cost minimization from PhysicsComplexityStructure and the discrete φ-tier structure from PhiForcingDerived.
proof idea
The proof unfolds isQuantum and isClassical, exposing the comparison of t against decoherenceTime env. It then applies the library lemma le_or_lt to obtain the disjunction of ≤ and <, followed by symmetry to match the target order. This is a direct one-line term proof that relies only on the total order of the reals.
why it matters
The result formalizes the complementary regimes stated in the module documentation for QF-009 and supplies the logical boundary used by sibling declarations such as decoherence_decreases_with_modes and gap_range. It connects the φ-scaling of decoherence times to the eight-tick octave and D=3 spatial structure of the broader Recognition Science framework. No downstream theorems are listed, leaving open the question of how the dichotomy integrates with explicit measurement postulates.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.