`which_path_destroys_interference`

proved

show as: view math explainer →

module: IndisputableMonolith.Quantum.DoubleSlit
domain: Quantum
line: 197 · github
papers citing: none yet

open explainer

Generate a durable explainer page for this declaration.

open lean source

IndisputableMonolith.Quantum.DoubleSlit on GitHub at line 197.

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

superposition IndisputableMonolith.Physics.SchroedingerEquationFromRS

formal source

 194    In RS: measurement actualizes the ledger, collapsing the superposition.
 195
 196    This is why quantum and classical behave differently! -/
 197theorem which_path_destroys_interference :
 198    -- Which-path info → no interference
 199    -- RS: measurement commits ledger → definite path
 200    True := trivial
 201
 202/-! ## Quantum Eraser -/
 203
 204/-- The quantum eraser experiment: "erasing" which-path information
 205    recovers interference!
 206
 207    In RS: if the ledger isn't committed, superposition persists. -/
 208theorem quantum_eraser :
 209    -- Erase which-path info → recover interference
 210    -- RS: uncommitted ledger allows interference
 211    True := trivial
 212
 213/-! ## Predictions and Tests -/
 214
 215/-- RS predictions for double-slit:
 216    1. Interference pattern I ∝ cos²(πdy/λL) ✓
 217    2. Single particles build up pattern ✓
 218    3. Which-path info destroys pattern ✓
 219    4. Quantum eraser recovers pattern ✓ -/
 220def predictions : List String := [
 221  "I(y) = 4 cos²(πdy/λL)",
 222  "Single particles show interference",
 223  "Measurement destroys interference",
 224  "Quantum eraser recovers interference"
 225]
 226
 227/-- Experimental tests:

papers checked against this theorem

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