fringeSpacing
plain-language theorem explainer
fringeSpacing defines the distance between adjacent bright fringes as the product of wavelength and screen distance divided by slit separation. Physicists reconstructing quantum interference from Recognition Science phase rules would cite this when converting path differences into observable positions on the screen. It is realized as a direct arithmetic combination of the three parameters stored in DoubleSlitSetup.
Claim. Given a double-slit setup with positive slit separation $d$, screen distance $L$, and wavelength $lambda$, the fringe spacing is $Delta y = lambda L / d$.
background
DoubleSlitSetup is a structure holding slit separation $d$, screen distance $L$, and wavelength $lambda$, each required to be positive. The module derives double-slit interference from Recognition Science's 8-tick phase accumulation: two paths accumulate phases whose difference depends on path length, producing intensity proportional to $2 + 2cos(Delta phi)$. Upstream results include the lambda normalization from RGTransport and forcing structures from UniversalForcingSelfReference, though the present definition directly encodes the geometric fringe-spacing formula.
proof idea
This is a one-line definition that multiplies the wavelength field by the screen-distance field and divides by the slit-separation field.
why it matters
It supplies the spacing value required by the bright_fringes and dark_fringes theorems to locate positions of maximum and zero intensity. The definition fills the QF-012 target of obtaining the interference pattern from 8-tick phase structure. It connects to the eight-tick octave landmark by giving the observable scale of phase-driven fringes on the screen.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.