pathLength1
plain-language theorem explainer
pathLength1 supplies the Euclidean distance from source through the first slit (at offset -d/2) to screen coordinate y. Modelers assembling double-slit amplitudes in Recognition Science cite it when forming the two-path sum for intensity. The definition is a direct one-line realization of the Pythagorean distance in the setup geometry.
Claim. Given DoubleSlitSetup parameters with slit separation $d > 0$ and screen distance $L > 0$, the path length through slit 1 to screen position $y$ is $L^2 + (y - d/2)^2$ under the square root.
background
The module derives double-slit interference from Recognition Science's 8-tick phase accumulation: two paths accumulate phases whose difference yields the cosine intensity pattern. DoubleSlitSetup packages the geometric inputs d (slit separation), L (screen distance), and lambda (wavelength) together with positivity proofs. Upstream results include the structure definition itself and the point interval constructor; the Recognition L ledger definitions supply the broader phase context but are not invoked in the distance formula.
proof idea
One-line definition that applies the Euclidean distance formula directly to the vertical offset y - d/2 and the fixed screen distance L.
why it matters
The definition is invoked inside amplitude to supply the two path lengths whose phases are exponentiated and summed. It supplies the geometric input required by the module's QF-012 derivation of fringe spacing from 8-tick phase structure. No open scaffolding is closed here; the result is a supporting geometric primitive.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.