cos_int_mul_pi_sq
plain-language theorem explainer
The lemma proves that the square of the cosine of any integer multiple of pi equals one. Quantum modelers working from Recognition Science's 8-tick phase would cite it to confirm unit intensity at constructive interference maxima. The proof is a one-line wrapper that reduces the cosine via a library identity then squares the resulting power of negative one.
Claim. For any integer $n$, $ (cos(n π))^2 = 1 $.
background
The DoubleSlit module derives interference from 8-tick phase accumulation on two paths, giving intensity proportional to 2 + 2 cos(Δφ) with constructive maxima when Δφ = 2nπ. This lemma supplies the required trigonometric reduction at those points. The upstream neg_one_zpow_sq proves ((-1 : ℝ)^n)^2 = 1 by direct expansion and the fact that (-1) * (-1) = 1. The module setting is QF-012, which links the observed double-slit pattern to the eight-tick octave of the forcing chain.
proof idea
The proof is a one-line wrapper. It rewrites cos(n π) to (-1)^n using Real.cos_int_mul_pi, then applies the exact lemma neg_one_zpow_sq to obtain the square equal to 1.
why it matters
The identity is invoked inside bright_fringes to conclude that intensity equals 4 at y = n × Δy. It thereby closes the algebraic verification that the 8-tick phase structure reproduces the classical interference pattern. The result sits at the interface between the eight-tick octave (T7) and the concrete quantum prediction, confirming that no extra postulates are needed for the bright-fringe locations.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.