def definition def or abbrev

`destructive_interference`

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

formal statement (Lean)

 190def destructive_interference (path1 path2 : List Config) : Prop :=

Definition body.

 191  ∃ n : ℤ, interference_amplitude path1 path2 (Real.pi * (2 * n + 1)) < 0
 192
 193/-- Constructive interference at phase 0. -/

Lean names referenced from this declaration's body.