def definition def or abbrev

`predictions`

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

formal statement (Lean)

 220def predictions : List String := [

proof body

Definition body.

 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:
 228    1. Young's original experiment (1801) - light ✓
 229    2. Davisson-Germer (1927) - electrons ✓
 230    3. Zeilinger et al. - fullerenes ✓
 231    4. Delayed-choice quantum eraser - photons ✓ -/

depends on (6)

Lean names referenced from this declaration's body.

Measurement in IndisputableMonolith.Data.Import decl_use
tests in IndisputableMonolith.ILG.CPMInstance decl_use
Measurement in IndisputableMonolith.Measurement.RSNative.Core decl_use
Measurement in IndisputableMonolith.Quantum.NonlocalityNoSignaling decl_use
L in IndisputableMonolith.Recognition decl_use
L in IndisputableMonolith.Recognition.Cycle3 decl_use