localWeylMonomial_phase_orthogonal
plain-language theorem explainer
For fixed shift a on the ququart, the local Weyl monomials with distinct phase labels b ≠ b' are orthogonal under the Hilbert-Schmidt inner product on single-core operators. Researchers constructing orthonormal bases for the finite Weyl representation in Recognition Science cores would cite this when decomposing local operators. The proof unfolds the inner product, reduces each summand via the explicit action on basis kets, expands the four-term sum, and discharges all cases by finite enumeration plus ring simplification.
Claim. Fix $a,b,b' : {0,1,2,3}$ with $b ≠ b'$. Then the local operator inner product satisfies $⟨W_a^b, W_a^{b'}⟩ = 0$, where $W_a^b$ is the linear operator on the ququart given by $(W_a^b ψ)(s) = i^{b·s} ψ(s-a mod 4)$ and the inner product is the sum over the four standard basis vectors of the conjugate-transpose product of the two operators.
background
The module models a single recognition core on the four-dimensional ququart with basis kets indexed by Fin 4. Addition modulo 4 is realized by add4, while localWeylMonomial (a b) encodes the Weyl monomial X^a Z^b acting by phase multiplication followed by a shift. The localOperatorInner supplies the Hilbert-Schmidt pairing on these operators via a double sum over basis vectors. Upstream, localWeylMonomial_basisKet records that the monomial maps a basis ket to a phased shifted basis ket, and scaled_basisKet_inner gives the inner product of two such scaled vectors.
proof idea
Unfold localOperatorInner to obtain a sum over s of the product of the two phase factors. For each s invoke scaled_basisKet_inner (after substituting the explicit action from localWeylMonomial_basisKet) to replace the summand by (-I)^{b·(a+s)} · I^{b'·(a+s)}. Expand the four-term sum with Fin.sum_univ_four, then apply fin_cases on a, b, b' together with simp, ring_nf, neg_I_pow and I_pow_five; every case with b ≠ b' reduces to zero.
why it matters
The result supplies the equal-shift case required by the downstream theorem localWeylMonomial_orthogonal_of_ne, which asserts full orthogonality for any distinct one-core Weyl labels. It therefore contributes the phase-orthogonality block needed to obtain an orthonormal operator basis on the ququart, supporting the decomposition of coupled recognition cores. Within the broader framework this closes one branch of the local Weyl representation used to realize the eight-tick octave structure on finite cores.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.