bright_fringes
plain-language theorem explainer
The theorem shows that intensity reaches its maximum value of 4 at screen positions that are integer multiples of the fringe spacing in a double-slit setup. Researchers deriving interference patterns from 8-tick phase accumulation in Recognition Science would cite this result. The proof unfolds the intensity and phase expressions, reduces the accumulated phase difference to nπ by field simplification under the positivity hypotheses, and applies the cosine identity at integer multiples of π together with a multiplication lemma.
Claim. Let $d, L, λ > 0$ be slit separation, screen distance and wavelength. Let $Δy = λ L / d$ be the fringe spacing. Then the intensity at position $y = n Δy$ for integer $n$ equals 4, since the phase difference equals $2nπ$ and the intensity formula yields $2 + 2 cos(2nπ) = 4$.
background
The module derives the double-slit pattern from Recognition Science's 8-tick phase structure. Each path accumulates phases of the form $kπ/4$ for $k = 0..7$, and the phase difference $Δφ$ between the two slits depends on the geometric path difference. Intensity is defined as $2 + 2 cos(Δφ)$, reaching its maximum of 4 when $Δφ = 2nπ$ (constructive interference) and zero when $Δφ = (2n+1)π$ (destructive). The DoubleSlitSetup structure packages the three positive real parameters $d, L, λ$ together with their positivity proofs. Upstream, the EightTick.phase definition supplies the periodic $kπ/4$ values, while ArithmeticFromLogic.mul_one supplies the algebraic identity used in the final simplification step.
proof idea
The tactic proof first unfolds intensity, phaseDifference, pathDifference and fringeSpacing. It introduces three non-zero hypotheses via ne_of_gt on the positivity fields of the setup. A field_simp step then reduces the explicit phase expression $2π (d · (n · (λ L / d)) / L) / λ / 2$ to $nπ$. The final simp applies the identity cos_int_mul_pi_sq together with mul_one to conclude that the cosine-squared term equals 1, yielding intensity = 4.
why it matters
This result fills the constructive-interference half of the QF-012 double-slit derivation, confirming that the 8-tick phase model reproduces the textbook bright-fringe locations and maximum intensity. It sits inside the eight-tick octave (T7) and supplies the interference pattern required for later amplitude and probability calculations. No downstream theorems yet depend on it, leaving open the question of how the same phase structure extends to multi-slit or diffraction cases.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.