phaseDifference
plain-language theorem explainer
Phase difference between paths in a double-slit setup equals 2π times the geometric path difference divided by wavelength. Quantum modelers working from Recognition Science's eight-tick phase accumulation cite this to obtain the cosine-squared intensity law. It is a direct one-line definition that supplies the argument to the amplitude sum.
Claim. $Δφ(y) = 2π ⋅ ΔL(y) / λ$, where ΔL(y) denotes the path difference for a setup with slit separation d > 0, screen distance L > 0, and wavelength λ > 0.
background
DoubleSlitSetup is the structure holding slit separation d, screen distance L, and wavelength λ, all required positive. The module derives the interference pattern from Recognition Science's eight-tick phase structure: two paths accumulate phases, their difference controls constructive or destructive addition, and probability follows |e^{iφ_L} + e^{iφ_R}|^2 = 2 + 2 cos(Δφ). Upstream results supply the ledger factorization and φ-power balance used to ground the phase accumulation in the broader forcing chain.
proof idea
One-line definition that multiplies the path difference by 2π and divides by lambda.
why it matters
This definition supplies the phase argument to intensity, bright_fringes, dark_fringes, and max_intensity. It fills the step that converts geometric path lengths into the 8-tick phase difference required by the module's target derivation of interference from the eight-tick octave (T7). Downstream theorems then recover the standard bright-fringe condition Δφ = 2nπ and the fringe spacing λL/d.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.