theorem proved term proof

`quantum_classical_dichotomy`

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

formal statement (Lean)

 149theorem quantum_classical_dichotomy (env : EnvironmentCoupling) (t : ℝ) :
 150    isQuantum env t ∨ isClassical env t := by

proof body

Term-mode proof.

 151  unfold isQuantum isClassical
 152  exact le_or_lt (decoherenceTime env) t |>.symm
 153
 154/-! ## Critical Number of Modes -/
 155
 156/-- The critical number of modes at which decoherence equals a given timescale.
 157    Solve: τ_0 × φ^(-N × g) = τ_target
 158    → N = -ln(τ_target/τ_0) / (g × ln(φ)) -/

depends on (12)

Lean names referenced from this declaration's body.

of in IndisputableMonolith.Astrophysics.NucleosynthesisTiers decl_use
modes in IndisputableMonolith.ClassicalBridge.Fluids.Galerkin2D decl_use
of in IndisputableMonolith.Foundation.DAlembert.LedgerFactorization decl_use
of in IndisputableMonolith.Foundation.PhiForcingDerived decl_use
of in IndisputableMonolith.Foundation.SpectralEmergence decl_use
of in IndisputableMonolith.Information.PhysicsComplexityStructure decl_use
decoherenceTime in IndisputableMonolith.QFT.Decoherence decl_use
EnvironmentCoupling in IndisputableMonolith.QFT.Decoherence decl_use
isClassical in IndisputableMonolith.QFT.Decoherence decl_use
isQuantum in IndisputableMonolith.QFT.Decoherence decl_use
decoherenceTime in IndisputableMonolith.Quantum.ClassicalEmergence decl_use
decoherenceTime in IndisputableMonolith.Quantum.PointerStates decl_use