fringeSpacing

formal source

 118
 119/-- The fringe spacing (distance between bright fringes).
 120    Δy = λL / d -/
 121noncomputable def fringeSpacing (setup : DoubleSlitSetup) : ℝ :=
 122  setup.lambda * setup.L / setup.d
 123
 124/-! ### Helper lemmas for interference proofs -/
 125
 126/-- (-1)^n squared is 1 for any integer n. -/
 127private lemma neg_one_zpow_sq (n : ℤ) : ((-1 : ℝ) ^ n) ^ 2 = 1 := by
 128  have h : (-1 : ℝ) * (-1 : ℝ) = 1 := by norm_num
 129  calc ((-1 : ℝ) ^ n) ^ 2 = ((-1 : ℝ) ^ n * (-1 : ℝ) ^ n) := sq _
 130    _ = ((-1 : ℝ) * (-1 : ℝ)) ^ n := (mul_zpow (-1) (-1) n).symm
 131    _ = 1 ^ n := by rw [h]
 132    _ = 1 := one_zpow n
 133
 134/-- cos(nπ)² = 1 for any integer n. -/
 135private lemma cos_int_mul_pi_sq (n : ℤ) : Real.cos (n * π) ^ 2 = 1 := by
 136  rw [Real.cos_int_mul_pi]
 137  exact neg_one_zpow_sq n
 138
 139/-- cos((2n+1)π/2) = 0 for any integer n. -/
 140private lemma cos_half_odd_mul_pi (n : ℤ) : Real.cos ((2 * n + 1) * π / 2) = 0 := by
 141  have h : (2 * n + 1) * π / 2 = π / 2 + n * π := by ring
 142  rw [h, Real.cos_add, Real.cos_pi_div_two, Real.sin_pi_div_two]
 143  simp [Real.sin_int_mul_pi]
 144
 145/-- **THEOREM**: Bright fringes occur at y = n × Δy with maximum intensity.
 146    At these positions, the phase difference is 2nπ, giving cos²(nπ) = 1.  -/
 147theorem bright_fringes (setup : DoubleSlitSetup) (n : ℤ) :
 148    intensity setup (n * fringeSpacing setup) = 4 := by
 149  unfold intensity phaseDifference pathDifference fringeSpacing
 150  have hd : setup.d ≠ 0 := ne_of_gt setup.d_pos
 151  have hL : setup.L ≠ 0 := ne_of_gt setup.L_pos