intensity_oscillates
plain-language theorem explainer
The declaration shows that intensity at screen position y equals four times the square of the cosine of half the phase difference for any double-slit setup. Researchers deriving quantum interference from Recognition Science's eight-tick phase accumulation would reference this identity. The proof proceeds by direct reflexivity from the definition of intensity.
Claim. For a double-slit setup with slit separation $d$, screen distance $L$, and wavelength $lambda$, the intensity $I(y)$ at position $y$ on the screen satisfies $I(y) = 4 cos^2 (Delta phi(y)/2)$, where $Delta phi(y)$ is the phase difference between the two paths.
background
The module QF-012 derives double-slit interference from Recognition Science's 8-tick phase structure. Two paths accumulate phases whose difference $Delta phi$ depends on path length; probability is proportional to $2 + 2 cos(Delta phi)$. DoubleSlitSetup is the structure holding slit separation $d > 0$, screen distance $L > 0$, and wavelength $lambda > 0$. The intensity definition computes $4 (cos (Delta phi / 2))^2$ directly from phaseDifference.
proof idea
The proof is a one-line reflexivity that equates the intensity function to its defining expression involving the cosine of the phase difference.
why it matters
This theorem completes the derivation of the standard interference pattern within the Recognition Science framework, linking the 8-tick phase accumulation (T7) to the observed cos² intensity modulation. It supports the module's target of deriving interference from RS phase structure, as outlined in the Foundations of Physics paper proposition. No downstream uses are recorded yet, but it underpins further results like maximum intensity.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.