cos_half_odd_mul_pi
plain-language theorem explainer
The lemma shows that cosine vanishes at every odd multiple of π/2 for integer n. Modelers of double-slit interference in the Recognition Science setting cite it when locating dark fringes. The proof rewrites the argument via ring, applies the cosine addition formula, and reduces the result with standard values of sine and cosine at multiples of π.
Claim. For any integer $n$, $cos(((2n+1)π)/2)=0$.
background
The DoubleSlit module derives interference from 8-tick phase accumulation along two paths, where each path contributes phases of the form kπ/4. The upstream phase definition supplies these discrete increments and states that the phase is 2π-periodic. This lemma supplies the trigonometric identity needed to evaluate intensity when the path difference produces an odd multiple of π.
proof idea
The tactic proof first rewrites the argument as π/2 + nπ by ring. It then rewrites using the cosine addition formula together with the known values cos(π/2)=0 and sin(π/2)=1. The remaining term is reduced by simp using the fact that sine of any integer multiple of π is zero.
why it matters
The identity is applied directly by the downstream dark_fringes theorem to establish zero intensity at half-integer positions. It completes the derivation of the full fringe pattern in the QF-012 module, connecting the eight-tick octave (T7) to observable destructive interference. No open scaffolding remains for this step.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.