intensity
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.
claimFor 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 in Recognition Science
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.
scope and limits
- Does not derive path lengths from first principles.
- Does not enforce the 8-tick structure inside the formula.
- Does not compute fringe spacing or wavelength from RS constants.
- Does not address particle statistics or creation thresholds.
formal statement (Lean)
103noncomputable def intensity (setup : DoubleSlitSetup) (y : ℝ) : ℝ :=
proof body
Definition body.
104 let Δφ := phaseDifference setup y
105 4 * (Real.cos (Δφ / 2))^2
106
107/-- **THEOREM**: Intensity oscillates with cos². -/