intensity
plain-language theorem explainer
The intensity definition computes the probability density at screen position y for a double-slit experiment parameterized by slit separation d, screen distance L, and wavelength lambda. Researchers deriving interference patterns from the 8-tick phase model cite it to recover the standard cos squared fringe profile. It is a direct one-line reduction that substitutes the phase difference and applies the double-angle cosine identity.
Claim. For a double-slit setup with positive slit separation $d$, screen distance $L$, and wavelength $lambda$, the intensity at transverse position $y$ is $I(y) = 4 cos^2(Delta phi(y)/2)$, where $Delta phi(y) = 2 pi times pathDifference(y)/lambda$ and pathDifference is the geometric path length difference between the two slits.
background
The module QF-012 derives the double-slit interference pattern from Recognition Science's 8-tick phase accumulation on two paths. DoubleSlitSetup is the structure holding the three positive real parameters d (slit separation), L (screen distance), and lambda (wavelength). phaseDifference is the upstream definition that returns 2 pi times pathDifference divided by lambda, where pathDifference itself encodes the geometric excess length for a point at height y on the screen.
proof idea
One-line wrapper that binds the phase difference from the upstream definition and multiplies four by the square of the cosine of half that phase.
why it matters
This definition supplies the intensity formula used by the bright_fringes and dark_fringes theorems to locate maxima at intensity 4 and minima at intensity 0. It realizes the QF-012 core insight that interference arises from 8-tick phase accumulation, connecting directly to the T7 eight-tick octave in the forcing chain. It feeds downstream into amplitude, fringeSpacing, and cross-domain applications such as NarrativeGeodesic and RecognitionCategory domain instances.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.