module module

`IndisputableMonolith.Quantum.DoubleSlit`

show as: view Lean formalization →

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

generate prose now

depends on (1)

Lean names referenced from this declaration's body.

IndisputableMonolith.Constants module_import

declarations in this module (25)

structure DoubleSlitSetup L46
def electronSetup L59
def pathPhase L72
def pathLength1 L76
def pathLength2 L80
def pathDifference L84
def phaseDifference L89
def amplitude L96
def intensity L103
theorem intensity_oscillates L108
theorem max_intensity L112
def fringeSpacing L121
lemma neg_one_zpow_sq L127
lemma cos_int_mul_pi_sq L135
lemma cos_half_odd_mul_pi L140
theorem bright_fringes L147
theorem dark_fringes L159
theorem interference_from_8tick L179
theorem single_particle_interference L187
theorem which_path_destroys_interference L197
theorem quantum_eraser L208
def predictions L220
def experiments L232
structure DoubleSlitFalsifier L246
def experimentalStatus L253