pathLength2

formal source

  77  Real.sqrt (setup.L^2 + (y - setup.d/2)^2)
  78
  79/-- Path length from source through slit 2 to point y on screen. -/
  80noncomputable def pathLength2 (setup : DoubleSlitSetup) (y : ℝ) : ℝ :=
  81  Real.sqrt (setup.L^2 + (y + setup.d/2)^2)
  82
  83/-- Path length difference (small angle approximation). -/
  84noncomputable def pathDifference (setup : DoubleSlitSetup) (y : ℝ) : ℝ :=
  85  -- In small angle approximation: Δr ≈ d × sin(θ) ≈ d × y / L
  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