localWeylMonomial_shift_orthogonal
plain-language theorem explainer
Distinct shift indices a ≠ a' force the local Weyl monomials W_{a,b} and W_{a',b'} to be orthogonal under the Hilbert-Schmidt inner product on ququart operators, for any phase indices b and b'. Researchers constructing orthogonal bases for finite-dimensional Weyl operators or discrete quantum channels would cite this step. The proof unfolds the inner-product sum, uses add4 properties to show the shifted basis vectors differ for every summation index, and reduces each term to zero via the scaled-basis inner-product lemma.
Claim. Let $W_{a,b}$ be the local Weyl monomial operator on the ququart space. If $a ≠ a'$ in $ℤ/4ℤ$, then for all $b,b' ∈ ℤ/4ℤ$ the Hilbert-Schmidt inner product satisfies $⟨W_{a,b}, W_{a',b'}⟩_{HS} = 0$, where $⟨A,B⟩_{HS} = ∑_{s,t} (A |s⟩)_t^* (B |s⟩)_t$.
background
The module defines ququart states as maps Fin 4 → ℂ with standard basis vectors basisKet. The operator localWeylMonomial a b acts by sending ψ(s) to i^{b.val ⋅ s.val} ⋅ ψ(sub4 s a), the discrete analog of X^a Z^b. Its inner product is given by localOperatorInner, the explicit Hilbert-Schmidt pairing ∑_s ∑_t star(A (basisKet s) t) ⋅ B (basisKet s) t. Addition add4 is componentwise sum modulo 4; the companion lemma add4_eq_add4_iff_left states that add4 a s = add4 a' s if and only if a = a' for fixed s. The auxiliary lemma scaled_basisKet_inner evaluates the inner product of two scaled basis vectors and returns zero when the underlying kets differ.
proof idea
Unfold localOperatorInner and apply Finset.sum_eq_zero. For each summation index s, rewrite both operators on basisKet s via localWeylMonomial_basisKet to obtain scaled basis kets whose shifts are add4 a s and add4 a' s. Use add4_eq_add4_iff_left together with the hypothesis a ≠ a' to obtain add4 a s ≠ add4 a' s. Invoke scaled_basisKet_inner on the resulting phases and indices; the differing kets force the inner product term to vanish, completing the sum.
why it matters
The result is the key case in the proof of localWeylMonomial_orthogonal_of_ne, which asserts full orthogonality of the 16 local Weyl monomials whenever the label pairs differ. It therefore supplies the shift-distinct half of the orthogonal operator basis needed for the single-core Weyl representation inside CoupledRecognitionCores. In the Recognition Science setting this orthogonality underpins the discrete phase and shift structure that later couples to the eight-tick octave and the three-dimensional spatial embedding.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.