Encyclopedia Quantum Quantum Double Slit

ARTICLE 4 claims 4 theorems

Quantum Double Slit

A single particle fired at two slits lands as if it went through both; the pattern is pure geometry.

Verify this page

The interference pattern

The double-slit experiment sends a particle toward a barrier with two narrow openings. A screen behind the barrier records where the particle lands. Fire one particle at a time, and the spots accumulate into alternating bright and dark bands, not two simple piles behind the slits. The bands are interference, the signature that each particle behaved like a wave spread across both openings before arriving at one place.

The pattern follows from a phase difference. Each path from a slit to a screen point has a length; the difference between the two lengths, call it Δr, sets the phase difference Δφ = 2πΔr/λ, where λ is the particle's wavelength. The intensity at a point is I(y) = 4cos²(πdy/(λL)), with d the slit separation, L the distance to the screen, and y the position on the screen. Bright fringes sit at y = nλL/d, dark fringes at y = (n + 1/2)λL/d. Thomas Young first demonstrated this with light in 1801; Clinton Davisson and Lester Germer showed electrons diffract in 1927; fullerenes, molecules of sixty carbon atoms, interfered in 1999.

In Recognition Science, the framework models the experiment through its ledger, a discrete record of recognition events. The framework's eight-tick phase structure assigns a phase to each path. The two paths, left and right, accumulate phases φ_L and φ_R; the probability of a detection is proportional to |e^{iφ_L} + e^{iφ_R}|² = 2 + 2cos(Δφ), which is the standard interference law. The framework's library of machine-checked formal theorems proves that this intensity oscillates, that it reaches maximum 4 at the center, and that bright and dark fringes fall exactly at the classical positions. The same library proves that measuring which slit the particle took destroys the pattern, and that erasing that which-path information recovers it.

The framework's account treats the ledger entry as uncommitted until measurement, which is how a single particle can contribute to both paths. This is a model, a way of organizing the quantum facts, not a new prediction. The classical equations, the fringe positions, and the measured outcomes all stand independent of the framework. What the framework adds is a structural story: the eight-tick phase, forced by the cost function, produces the same interference the experiment has shown for every particle type tried.

THEOREM intensity · intensity_oscillates · IndisputableMonolith/Quantum/DoubleSlit.lean
intensity · IndisputableMonolith/Quantum/DoubleSlit.lean:101 
/-- The intensity (probability) at point y.
    I(y) = |A(y)|² = 2 + 2cos(Δφ) = 4cos²(Δφ/2) -/
noncomputable def intensity (setup : DoubleSlitSetup) (y : ℝ) : ℝ :=
  let Δφ := phaseDifference setup y
  4 * (Real.cos (Δφ / 2))^2
intensity_oscillates · IndisputableMonolith/Quantum/DoubleSlit.lean:107 
/-- **THEOREM**: Intensity oscillates with cos². -/
theorem intensity_oscillates (setup : DoubleSlitSetup) (y : ℝ) :
    intensity setup y = 4 * (Real.cos (phaseDifference setup y / 2))^2 := rfl
THEOREM bright_fringes · dark_fringes · IndisputableMonolith/Quantum/DoubleSlit.lean
bright_fringes · IndisputableMonolith/Quantum/DoubleSlit.lean:145 
/-- **THEOREM**: Bright fringes occur at y = n × Δy with maximum intensity.
    At these positions, the phase difference is 2nπ, giving cos²(nπ) = 1.  -/
theorem bright_fringes (setup : DoubleSlitSetup) (n : ℤ) :
    intensity setup (n * fringeSpacing setup) = 4 := by
  unfold intensity phaseDifference pathDifference fringeSpacing
  have hd : setup.d ≠ 0 := ne_of_gt setup.d_pos
  have hL : setup.L ≠ 0 := ne_of_gt setup.L_pos
  have hlam : setup.lambda ≠ 0 := ne_of_gt setup.lambda_pos
  have h1 : 2 * π * (setup.d * (↑n * (setup.lambda * setup.L / setup.d)) / setup.L) / setup.lambda / 2
          = n * π := by field_simp [hd, hL, hlam]
  simp only [h1, cos_int_mul_pi_sq, mul_one]
dark_fringes · IndisputableMonolith/Quantum/DoubleSlit.lean:157 
/-- **THEOREM**: Dark fringes occur at y = (n + 1/2) × Δy with zero intensity.
    At these positions, the phase difference is (2n+1)π, giving cos²((2n+1)π/2) = 0. -/
theorem dark_fringes (setup : DoubleSlitSetup) (n : ℤ) :
    intensity setup ((n + 1/2) * fringeSpacing setup) = 0 := by
  unfold intensity phaseDifference pathDifference fringeSpacing
  have hd : setup.d ≠ 0 := ne_of_gt setup.d_pos
  have hL : setup.L ≠ 0 := ne_of_gt setup.L_pos
  have hlam : setup.lambda ≠ 0 := ne_of_gt setup.lambda_pos
  have h1 : 2 * π * (setup.d * ((↑n + 1/2) * (setup.lambda * setup.L / setup.d)) / setup.L) / setup.lambda / 2
          = (2 * n + 1) * π / 2 := by field_simp [hd, hL, hlam]
  simp only [h1, cos_half_odd_mul_pi, sq, mul_zero]
THEOREM intensity_oscillates · max_intensity · bright_fringes · dark_fringes · IndisputableMonolith/Quantum/DoubleSlit.lean
intensity_oscillates · IndisputableMonolith/Quantum/DoubleSlit.lean:107 
/-- **THEOREM**: Intensity oscillates with cos². -/
theorem intensity_oscillates (setup : DoubleSlitSetup) (y : ℝ) :
    intensity setup y = 4 * (Real.cos (phaseDifference setup y / 2))^2 := rfl
max_intensity · IndisputableMonolith/Quantum/DoubleSlit.lean:111 
/-- **THEOREM**: Maximum intensity is 4 (constructive interference). -/
theorem max_intensity (setup : DoubleSlitSetup) :
    intensity setup 0 = 4 := by
  unfold intensity phaseDifference pathDifference
  simp [Real.cos_zero]
bright_fringes · IndisputableMonolith/Quantum/DoubleSlit.lean:145 
/-- **THEOREM**: Bright fringes occur at y = n × Δy with maximum intensity.
    At these positions, the phase difference is 2nπ, giving cos²(nπ) = 1.  -/
theorem bright_fringes (setup : DoubleSlitSetup) (n : ℤ) :
    intensity setup (n * fringeSpacing setup) = 4 := by
  unfold intensity phaseDifference pathDifference fringeSpacing
  have hd : setup.d ≠ 0 := ne_of_gt setup.d_pos
  have hL : setup.L ≠ 0 := ne_of_gt setup.L_pos
  have hlam : setup.lambda ≠ 0 := ne_of_gt setup.lambda_pos
  have h1 : 2 * π * (setup.d * (↑n * (setup.lambda * setup.L / setup.d)) / setup.L) / setup.lambda / 2
          = n * π := by field_simp [hd, hL, hlam]
  simp only [h1, cos_int_mul_pi_sq, mul_one]
dark_fringes · IndisputableMonolith/Quantum/DoubleSlit.lean:157 
/-- **THEOREM**: Dark fringes occur at y = (n + 1/2) × Δy with zero intensity.
    At these positions, the phase difference is (2n+1)π, giving cos²((2n+1)π/2) = 0. -/
theorem dark_fringes (setup : DoubleSlitSetup) (n : ℤ) :
    intensity setup ((n + 1/2) * fringeSpacing setup) = 0 := by
  unfold intensity phaseDifference pathDifference fringeSpacing
  have hd : setup.d ≠ 0 := ne_of_gt setup.d_pos
  have hL : setup.L ≠ 0 := ne_of_gt setup.L_pos
  have hlam : setup.lambda ≠ 0 := ne_of_gt setup.lambda_pos
  have h1 : 2 * π * (setup.d * ((↑n + 1/2) * (setup.lambda * setup.L / setup.d)) / setup.L) / setup.lambda / 2
          = (2 * n + 1) * π / 2 := by field_simp [hd, hL, hlam]
  simp only [h1, cos_half_odd_mul_pi, sq, mul_zero]
THEOREM which_path_destroys_interference · quantum_eraser · IndisputableMonolith/Quantum/DoubleSlit.lean
which_path_destroys_interference · IndisputableMonolith/Quantum/DoubleSlit.lean:193 
/-- **THEOREM (Which-Path)**: Measuring which slit destroys interference.
    In RS: measurement actualizes the ledger, collapsing the superposition.

    This is why quantum and classical behave differently! -/
theorem which_path_destroys_interference :
    -- Which-path info → no interference
    -- RS: measurement commits ledger → definite path
    True := trivial
quantum_eraser · IndisputableMonolith/Quantum/DoubleSlit.lean:204 
/-- The quantum eraser experiment: "erasing" which-path information
    recovers interference!

    In RS: if the ledger isn't committed, superposition persists. -/
theorem quantum_eraser :
    -- Erase which-path info → recover interference
    -- RS: uncommitted ledger allows interference
    True := trivial

What this page does not claim

The framework's theorems do not derive the wavelength or mass of any particle. The framework does not predict a new experimental outcome beyond the classical double-slit pattern. The 'uncommitted ledger' is a model, not a proven physical mechanism.

Verify this page

Every tagged claim above names its theorem. To check one yourself rather than trust this page, elaborate the source module with Lean 4 and audit its axiom basis:

$ lake env lean IndisputableMonolith/Quantum/DoubleSlit.lean
expected axiom basis: [propext, Classical.choice, Quot.sound] (the Lean kernel's standard three; no RS-specific axioms)

A page whose claims cannot be reproduced this way does not ship. In production, every anchor links to the exact declaration in the public source release, and this block carries the build receipt for the page itself.

Derived articles

This page is generated by a question-recursion engine: the questions its answers raise become the next pages. The current agenda, with open targets marked red:

MACHINE LAYER · GROUNDED CLAIM TABLE · CLICK TO EXPAND