neg_I_pow
plain-language theorem explainer
Powers of negative imaginary unit factor as negative one to the n times imaginary unit to the n. Researchers establishing phase orthogonality for local Weyl monomials in coupled recognition cores cite this identity to simplify inner-product calculations. The argument is a one-line algebraic rewrite that factors the base and applies the multiplicative exponent rule.
Claim. For every natural number $n$, $(-i)^n = (-1)^n i^n$.
background
The CoupledRecognitionCores module builds local operators on ququart states via basis kets and phase-labeled Weyl monomials. This lemma supplies a basic complex-arithmetic identity used inside phase-orthogonality arguments. No upstream results are required; the fact rests on the ring structure of the complexes.
proof idea
One-line wrapper that rewrites negative i as negative one times i by ring, then distributes the exponent via the multiplicative power rule.
why it matters
The identity is invoked inside localWeylMonomial_phase_orthogonal, which states that equal shifts but distinct phase labels are orthogonal in the one-core Weyl family. It removes explicit negative signs from phase factors, supporting the recognition composition law and phase calculations in the foundation layer.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.