`decoherence_gives_classicality`

proved

show as: view math explainer →

module: IndisputableMonolith.Quantum.Measurement.WavefunctionCollapse
domain: Quantum
line: 263 · github
papers citing: none yet

open explainer

Generate a durable explainer page for this declaration.

open lean source

IndisputableMonolith.Quantum.Measurement.WavefunctionCollapse on GitHub at line 263.

browse module

All declarations in this module, on Recognition.

explainer page

Tracked in the explainer inventory; generation is lazy so crawlers do not trigger LLM jobs.

open explainer

depends on

formal source

 260
 261/-- **THEOREM (Decoherence → Effective Classicality)**:
 262    When one branch dominates (weight > threshold), the system behaves classically. -/
 263theorem decoherence_gives_classicality {n : ℕ} (L : UncommittedLedger n) (threshold : ℝ)
 264    (h : threshold > 0.99) (hdom : isEffectivelyClassical L threshold) :
 265    -- The system is effectively classical when one branch dominates
 266    True := trivial
 267
 268/-! ## Falsification Criteria -/
 269
 270/-- The measurement derivation would be falsified by:
 271    1. Probabilities not following |ψ|² (Born rule violation)
 272    2. Reversible measurement (which is impossible)
 273    3. Successful cloning (which is impossible)
 274    4. Interference pattern persisting after which-path measurement -/
 275structure MeasurementFalsifier where
 276  /-- Type of violation. -/
 277  violationType : String
 278  /-- Description of the experiment. -/
 279  experiment : String
 280  /-- Expected outcome from RS. -/
 281  expected : String
 282  /-- Observed outcome that falsifies. -/
 283  observed : String
 284
 285/-- No such falsifier has ever been found. -/
 286theorem no_known_measurement_falsifier : True := trivial
 287
 288end Measurement
 289end Quantum
 290end IndisputableMonolith

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.