pathLength2
Defines the Euclidean path length from source through the second slit (offset +d/2) to screen point y. Physicists reconstructing double-slit fringes from Recognition Science phase accumulation cite this geometric primitive. It is a direct square-root expression using the setup parameters L and d.
claimThe path length through the second slit to screen coordinate $y$ equals $l_2(y) = L^2 + (y + d/2)^2$ under square root, where $d > 0$ is slit separation and $L > 0$ is distance from slits to screen.
background
DoubleSlitSetup is the parameter record holding slit separation $d$, screen distance $L$, and wavelength, each required positive. The module derives the double-slit pattern from 8-tick phase accumulation: two paths collect phases whose difference produces intensity $2 + 2 cos(Δφ)$ at the screen. Upstream DoubleSlitSetup supplies the concrete values of $d$ and $L$ that enter the distance formula.
proof idea
One-line definition that applies the Euclidean distance formula in the plane: vertical leg $L$, horizontal leg $y + d/2$.
why it matters in Recognition Science
Supplies the second path length required by the amplitude definition that sums the two complex exponentials. This geometric step precedes phase extraction and intensity oscillation inside the QF-012 derivation of interference from the 8-tick structure. It closes the classical path geometry before Recognition Science phase rules are applied.
scope and limits
- Does not incorporate wavelength.
- Does not compute accumulated phase.
- Does not invoke the small-angle approximation.
- Does not enforce positivity of the returned length.
Lean usage
let φ2 := pathPhase (pathLength2 setup y) setup.lambdaformal statement (Lean)
80noncomputable def pathLength2 (setup : DoubleSlitSetup) (y : ℝ) : ℝ :=
proof body
Definition body.
81 Real.sqrt (setup.L^2 + (y + setup.d/2)^2)
82
83/-- Path length difference (small angle approximation). -/