phaseDifference
plain-language theorem explainer
The phaseDifference definition supplies the phase shift between the two paths at screen position y as 2π times the geometric path difference divided by wavelength. Physicists working on interference within Recognition Science cite it when linking 8-tick phase accumulation to observable fringes. It is a direct algebraic definition that requires no lemmas beyond the pathDifference helper and feeds straight into intensity formulas.
Claim. For a double-slit setup with slit separation $d>0$, screen distance $L>0$, and wavelength $λ>0$, the phase difference at position $y$ is $Δφ(y)=2π⋅ΔL(y)/λ$, where $ΔL(y)$ is the path-length difference between the slits.
background
The module derives double-slit interference from Recognition Science's 8-tick phase structure: each path accumulates discrete phases, and interference arises from $|e^{iφ_L}+e^{iφ_R}|^2=2+2cos(Δφ)$. DoubleSlitSetup is the structure holding the three positive real parameters $d$, $L$, and $λ$. Upstream results supply the J-cost calibration and ledger factorization that fix the underlying phase accumulation in the broader framework.
proof idea
One-line definition that multiplies the path difference by $2π$ and divides by the wavelength taken from the setup record.
why it matters
This definition is invoked by intensity, bright_fringes, dark_fringes, and max_intensity to obtain the cos² oscillation with maxima of 4. It completes the QF-012 derivation of the interference pattern from the 8-tick phase (T7), connecting geometric path differences to probability amplitudes inside the Recognition Science framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.