dark_fringes
plain-language theorem explainer
The theorem shows that intensity vanishes at positions offset by half the fringe spacing in the double-slit setup. Researchers deriving quantum interference from Recognition Science's eight-tick phase would cite this result. The proof unfolds the intensity expression, reduces the phase difference to an odd multiple of pi over 2 via field simplification, and applies the cosine identity that forces zero intensity.
Claim. For a double-slit setup with slit separation $d > 0$, screen distance $L > 0$, and wavelength $lambda > 0$, the intensity at screen position $y = (n + 1/2) Delta y$ is zero for integer $n$, where $Delta y = lambda L / d$ is the fringe spacing.
background
DoubleSlitSetup is a structure holding the geometric parameters d for slit separation, L for screen distance, and lambda for wavelength, each required positive. Fringe spacing equals lambda times L divided by d. Intensity is computed from the squared cosine of half the phase difference between the two paths, with phase difference arising from path length difference over lambda times 2 pi. The module QF-012 derives the double-slit pattern from Recognition Science's 8-tick phase accumulation. Upstream results include the tick definition as the fundamental time quantum equal to 1 and the phase function assigning k pi over 4 for k from 0 to 7. This builds on the eight-tick octave in the forcing chain.
proof idea
The proof is a tactic proof that unfolds intensity, phaseDifference, pathDifference, and fringeSpacing. It introduces three hypotheses that d, L, and lambda are nonzero from their positivity assumptions. A field_simp step with those hypotheses reduces the cosine argument to (2 n + 1) pi over 2. Then simp applies the identity cos of half odd multiple of pi together with squaring and multiplication by zero to conclude intensity equals zero.
why it matters
This theorem completes the destructive interference case in the double-slit derivation within Recognition Science, confirming zero intensity at half-integer fringe positions from 8-tick phase steps. It supports the module target of obtaining the interference pattern from eight-tick phase accumulation as stated in the QF-012 documentation. The result aligns with T7 eight-tick octave in the forcing chain and contributes to showing quantum phenomena emerge from RS-native units and phase structure.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.