neg_one_zpow_sq
plain-language theorem explainer
The lemma proves that for any integer n the square of (-1) raised to n equals 1. Quantum modelers deriving double-slit fringe intensities from eight-tick phase accumulation cite it to simplify the squared cosine term in the intensity formula. The proof expands the square into a product of powers, folds the exponents via mul_zpow, substitutes the identity (-1) times (-1) equals 1, and reduces via one_zpow.
Claim. For any integer $n$, $[(-1)^n]^2 = 1$.
background
The DoubleSlit module derives the interference pattern from Recognition Science's 8-tick phase structure: two paths accumulate phases whose difference Δφ produces intensity proportional to 2 + 2 cos(Δφ). The lemma supplies the algebraic identity needed to confirm that cos(nπ)^2 equals 1, which appears when evaluating the oscillatory term at integer multiples of the base phase. It draws only on Mathlib real exponentiation and the module's import of Constants; the upstream structure for records meta-realization properties but is not invoked in the body.
proof idea
Tactic proof uses a calc chain. First rewrite the square as the product of two identical powers. Apply mul_zpow to obtain [(-1) * (-1)]^n. Substitute the norm_num fact that (-1) * (-1) = 1. Finish with one_zpow to reach 1.
why it matters
The result is called directly by cos_int_mul_pi_sq, which in turn supports intensity_oscillates and max_intensity in the double-slit derivation. It closes the elementary trigonometric reduction required by the T7 eight-tick octave in the forcing chain, ensuring the pattern alternates between constructive and destructive fringes exactly as predicted by the phase-difference formula.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.