localWeylMonomial_basisKet
plain-language theorem explainer
The theorem states that the local Weyl monomial operator maps each standard basis ket |s⟩ to a phase factor times the shifted ket |a + s mod 4⟩. Researchers computing matrix elements or inner products in the ququart Weyl-Heisenberg family cite this identity. The proof proceeds by function extensionality on the output index followed by case analysis on equality to the shifted label, using modular cancellation lemmas.
Claim. Let $W_{a,b}$ denote the local Weyl monomial operator on the ququart state space. For $a,b,s$ in the cyclic group of order 4, $W_{a,b} |s⟩ = i^{b(a+s)} |a+s⟩$, where $|m⟩$ is the standard basis vector that equals 1 at index $m$ and 0 elsewhere.
background
The ququart state space consists of functions from Fin 4 to ℂ. The definition basisKet m returns the indicator function that is 1 at m and 0 elsewhere. The operator localWeylMonomial a b is the linear map sending a state ψ to the function s ↦ i^{b·s} · ψ(sub4 s a), where sub4 and add4 implement subtraction and addition modulo 4. The upstream lemmas add4_sub4_cancel_core and sub4_add4_cancel_core establish that these operations are mutual inverses.
proof idea
The proof applies function extensionality to the output index m. It cases on whether m equals add4 a s. When equality holds, substitution and simplification invoke the definition of localWeylMonomial together with sub4_add4_cancel_core. When equality fails, the auxiliary claim sub4 m a ≠ s is derived via add4_sub4_cancel_core, forcing the result to zero.
why it matters
This supplies the explicit action of the local Weyl monomials on basis vectors and is invoked directly in the proofs of localWeylMonomial_self_inner, localWeylMonomial_phase_orthogonal, and localWeylMonomial_shift_orthogonal to evaluate Hilbert-Schmidt inner products. It completes the concrete representation needed for orthogonality statements inside the CoupledRecognitionCores module.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.