I_pow_star_mul_self
plain-language theorem explainer
The lemma establishes that i to any natural power has unit modulus, so its conjugate times itself equals one. It is cited inside the same module when proving Hilbert-Schmidt norms of local Weyl monomials. The proof is a short tactic sequence that reduces the claim to the known squared norm of i and the general identity normSq z = conj z * z.
Claim. For every natural number $n$, $i^n$ satisfies $i^n$ times its complex conjugate equals 1.
background
The declaration sits in CoupledRecognitionCores, a module that builds ququart states, basis kets, and local Weyl operators on top of the Recognition Science structures. It draws on the J-cost convexity and 8-tick local dynamics supplied by the PhysicsComplexityStructure and SpectralEmergence structures, together with the phase-lift machinery from CirclePhaseLift. The lemma supplies a basic algebraic fact about unit-modulus phases that appears when inner products of these operators are expanded.
proof idea
The tactic proof first simplifies the squared norm of i^n to 1 by invoking the library fact for i itself. It then applies the general identity that squared norm equals conjugate times the element, rewrites the known value of 1 into that identity, and concludes by symmetry.
why it matters
The result is used directly by localWeylMonomial_self_inner to obtain the Hilbert-Schmidt norm squared equal to 4 for each local Weyl monomial. It therefore supports the algebraic layer that connects the phi-ladder and the eight-tick octave to concrete operator calculations in the foundation. No open scaffolding questions are closed by this step.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.