fringeSpacing
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.
claimGiven 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 in Recognition Science
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.
scope and limits
- Does not derive wavelength from Recognition Science constants such as phi.
- Does not incorporate finite slit width or single-slit diffraction envelope.
- Does not address multi-particle or relativistic corrections.
- Does not prove the intensity oscillation formula itself.
Lean usage
theorem bright_fringes (setup : DoubleSlitSetup) (n : ℤ) : intensity setup (n * fringeSpacing setup) = 4 := by unfold intensity phaseDifference pathDifference fringeSpacingformal statement (Lean)
121noncomputable def fringeSpacing (setup : DoubleSlitSetup) : ℝ :=
proof body
Definition body.
122 setup.lambda * setup.L / setup.d
123
124/-! ### Helper lemmas for interference proofs -/
125
126/-- (-1)^n squared is 1 for any integer n. -/