pathLength1
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.
claimFor 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 in Recognition Science
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.
scope and limits
- Does not incorporate wavelength or phase accumulation.
- Does not compute the path difference between the two slits.
- Does not enforce positivity of the computed length beyond setup assumptions.
- Does not model wave propagation or quantum superposition.
Lean usage
let φ1 := pathPhase (pathLength1 setup y) setup.lambdaformal statement (Lean)
76noncomputable def pathLength1 (setup : DoubleSlitSetup) (y : ℝ) : ℝ :=
proof body
Definition body.
77 Real.sqrt (setup.L^2 + (y - setup.d/2)^2)
78
79/-- Path length from source through slit 2 to point y on screen. -/