def
definition
phaseDifference
show as:
view math explainer →
open explainer
Generate a durable explainer page for this declaration.
open lean source
IndisputableMonolith.Quantum.DoubleSlit on GitHub at line 89.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
-
of -
of -
A -
is -
of -
is -
of -
is -
of -
A -
is -
Pattern -
A -
point -
Pattern -
lambda -
amplitude -
two -
amplitude -
DoubleSlitSetup -
pathDifference -
Pattern -
Pattern
used by
formal source
86 setup.d * y / setup.L
87
88/-- Phase difference between the two paths. -/
89noncomputable def phaseDifference (setup : DoubleSlitSetup) (y : ℝ) : ℝ :=
90 2 * π * pathDifference setup y / setup.lambda
91
92/-! ## Interference Pattern -/
93
94/-- The amplitude at point y is the sum of two complex amplitudes.
95 A(y) = e^{iφ₁} + e^{iφ₂} -/
96noncomputable def amplitude (setup : DoubleSlitSetup) (y : ℝ) : ℂ :=
97 let φ1 := pathPhase (pathLength1 setup y) setup.lambda
98 let φ2 := pathPhase (pathLength2 setup y) setup.lambda
99 Complex.exp (I * φ1) + Complex.exp (I * φ2)
100
101/-- The intensity (probability) at point y.
102 I(y) = |A(y)|² = 2 + 2cos(Δφ) = 4cos²(Δφ/2) -/
103noncomputable def intensity (setup : DoubleSlitSetup) (y : ℝ) : ℝ :=
104 let Δφ := phaseDifference setup y
105 4 * (Real.cos (Δφ / 2))^2
106
107/-- **THEOREM**: Intensity oscillates with cos². -/
108theorem intensity_oscillates (setup : DoubleSlitSetup) (y : ℝ) :
109 intensity setup y = 4 * (Real.cos (phaseDifference setup y / 2))^2 := rfl
110
111/-- **THEOREM**: Maximum intensity is 4 (constructive interference). -/
112theorem max_intensity (setup : DoubleSlitSetup) :
113 intensity setup 0 = 4 := by
114 unfold intensity phaseDifference pathDifference
115 simp [Real.cos_zero]
116
117/-! ## Fringe Spacing -/
118
119/-- The fringe spacing (distance between bright fringes).