max_intensity
plain-language theorem explainer
The theorem states that intensity reaches its peak value of 4 at the screen center for any valid double-slit setup. Researchers deriving interference patterns from Recognition Science phase accumulation would cite this to anchor the bright-fringe maximum. The proof is a direct term reduction that unfolds the intensity definition and applies the cosine-zero identity.
Claim. For any double-slit setup with slit separation $d>0$, screen distance $L>0$, and wavelength $λ>0$, the intensity at screen position $y=0$ equals 4.
background
DoubleSlitSetup packages the three geometric parameters of the experiment together with positivity constraints. Intensity at screen position y is defined as 4 cos²(Δφ/2), where Δφ is the phase difference between the two paths. Path difference itself is the small-angle approximation d y / L, and phase difference is 2π times that quantity divided by λ. The module derives the entire interference pattern from the eight-tick phase structure of Recognition Science, with constructive interference when Δφ = 2nπ.
proof idea
The term proof unfolds intensity, phaseDifference, and pathDifference in sequence, then invokes simp with the Real.cos_zero lemma to reduce the expression at y=0 directly to 4.
why it matters
This result fixes the constructive-interference maximum inside the QF-012 derivation of double-slit fringes from eight-tick phase accumulation. It supplies the normalization constant needed for the subsequent fringe-spacing theorem in the same module and aligns with the T7 eight-tick octave landmark. No open scaffolding remains for this specific claim.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.