electronSetup

formal source

  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 : ℝ) : ℝ :=
  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 : ℝ) : ℝ :=