pathLength1
plain-language theorem explainer
The definition computes the Euclidean distance from source through the first slit to screen point y using the setup parameters. Modelers of interference in Recognition Science cite it to obtain the geometric input for phase differences in the 8-tick cycle. It is realized as a direct one-line application of the real square root to the Pythagorean sum of screen distance and slit offset.
Claim. For a double-slit setup with slit separation $d > 0$ and screen distance $L > 0$, the path length from the source through slit 1 to screen point $y$ is given by $L^2 + (y - d/2)^2$ under the square root.
background
The DoubleSlitSetup structure packages the slit separation $d$, screen distance $L$, and wavelength, each required positive, to formalize the experiment geometry. This definition supplies the length for the path through the first slit, which feeds the phase calculation in the module's derivation of interference from 8-tick phase accumulation. The module documentation states the core insight that interference emerges from phase differences between the two paths under the Recognition Science 8-tick structure.
proof idea
One-line definition that applies the real square root directly to the sum of the squared screen distance and the squared offset from the slit position at $d/2$.
why it matters
This supplies one path length to the amplitude definition, which combines phases from both slits to produce intensity. It fills the geometric step in the QF-012 derivation of double-slit fringes from the eight-tick octave. The parent result is the amplitude computation that yields the oscillatory intensity pattern.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.