DoubleSlitSetup

formal source

  43/-! ## The Setup -/
  44
  45/-- Parameters for a double-slit experiment. -/
  46structure DoubleSlitSetup where
  47  /-- Slit separation (meters). -/
  48  d : ℝ
  49  /-- Distance to screen (meters). -/
  50  L : ℝ
  51  /-- Wavelength of particle (meters). -/
  52  lambda : ℝ
  53  /-- All positive. -/
  54  d_pos : d > 0
  55  L_pos : L > 0
  56  lambda_pos : lambda > 0
  57
  58/-- A standard setup for electrons. -/
  59noncomputable def electronSetup : DoubleSlitSetup := {
  60  d := 1e-6,      -- 1 μm slit separation
  61  L := 1,         -- 1 m to screen
  62  lambda := 1e-9, -- ~1 nm wavelength (for keV electrons)
  63  d_pos := by norm_num,
  64  L_pos := by norm_num,
  65  lambda_pos := by norm_num
  66}
  67
  68/-! ## Path Phases -/
  69
  70/-- The phase accumulated along a path of length r.
  71    φ = 2π × r / λ = k × r (where k = 2π/λ) -/
  72noncomputable def pathPhase (r lambda : ℝ) : ℝ :=
  73  2 * π * r / lambda
  74
  75/-- Path length from source through slit 1 to point y on screen. -/
  76noncomputable def pathLength1 (setup : DoubleSlitSetup) (y : ℝ) : ℝ :=