pathDifference
plain-language theorem explainer
The pathDifference definition computes the approximate path length difference between slits to a screen point y under small-angle geometry. Researchers deriving interference from Recognition Science's 8-tick phase accumulation cite it when linking setup parameters to phase difference. It is implemented as a direct arithmetic expression from slit separation and screen distance.
Claim. $Δr = d y / L$ where $d$ is slit separation, $L$ is screen distance, and $y$ is transverse position on the screen.
background
The DoubleSlitSetup structure holds slit separation $d$, screen distance $L$, and wavelength $λ$, each required positive. This module derives double-slit interference from 8-tick phase accumulation, where each path collects phases from the Fin 8 cycle defined in upstream EightTick and ChurchTuringPhysicsStructure results. The module doc states that phase difference $Δφ$ depends on path length, yielding intensity proportional to $2 + 2 cos(Δφ)$.
proof idea
The definition is a direct one-line expression that applies the small-angle approximation $Δr ≈ d × y / L$ to the fields of the DoubleSlitSetup record. No lemmas or tactics are invoked; the body is pure arithmetic on the real parameters.
why it matters
pathDifference supplies the geometric input to phaseDifference, which is unfolded in the bright_fringes and dark_fringes theorems to locate intensity maxima and minima. It realizes the path-length term in the 8-tick phase model of the module, connecting to the eight-tick octave (T7) and the forcing chain that fixes three spatial dimensions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.