I_pow_five
plain-language theorem explainer
The lemma asserts that the imaginary unit raised to the fifth power equals the imaginary unit itself. Researchers handling phase factors in ququart states and local Weyl operators cite this reduction when simplifying exponents in inner-product calculations. The proof is a one-line wrapper invoking the general power-modulo identity for the imaginary unit.
Claim. $i^5 = i$ in the complex numbers, where $i = 0 + 1i$.
background
The CoupledRecognitionCores module defines ququart states, basis kets, and local Weyl monomials that employ complex phases for operator inner products. It imports structures for nuclear densities from nucleosynthesis tiers, J-cost calibration from ledger factorization, phi-ladder forcing, spectral emergence of gauge groups and generations, convex J-cost minimization, and spin-2 assignments. These supply the algebraic setting in which fifth-power reductions of $i$ appear during phase orthogonality arguments.
proof idea
The proof is a one-line wrapper that applies Complex.I_pow_eq_pow_mod to the exponent 5 and lets simpa discharge the resulting equality.
why it matters
The lemma feeds the localWeylMonomial_phase_orthogonal theorem, which shows that equal shifts with distinct phase labels remain orthogonal in the one-core Weyl family. It supplies a routine algebraic reduction inside the foundation layer that supports phase handling for the eight-tick octave and spectral emergence of SU(3) x SU(2) x U(1) content. No open scaffolding questions are addressed.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.