localWeylMonomial_self_inner
plain-language theorem explainer
Local Weyl monomials on a single ququart core satisfy Hilbert-Schmidt norm squared equal to four. Researchers normalizing finite-dimensional operator bases for coupled recognition models cite this when scaling Weyl-Heisenberg generators before multi-core assembly. The proof unfolds the inner-product definition, shows each of four basis inputs contributes a phase-cancelled unit term via explicit action and modulus lemmas, then sums them directly.
Claim. For any $a,b$ in the cyclic group of order 4, let $W_{a,b}$ be the linear operator on ququart states defined by $W_{a,b}ψ(s) = i^{b·s} ψ(s-a)$ (indices mod 4). Then the Hilbert-Schmidt inner product of $W_{a,b}$ with itself equals 4.
background
In the CoupledRecognitionCores module, ququart states are maps from Fin 4 to ℂ that serve as single-core carriers. The local Weyl monomial is the operator sending ψ to the function s ↦ i^(b·s) ψ(s-a mod 4), realizing a discrete X^a Z^b generator. localOperatorInner is the Hilbert-Schmidt pairing ∑_s ∑_t conj(A(basisKet s) t) · B(basisKet s) t, which reduces to a sum over the standard basis because the basis kets are orthonormal by construction.
proof idea
The proof unfolds localOperatorInner, then proves an auxiliary claim that each of the four basis inputs s contributes exactly 1 to the sum. For each s it substitutes the explicit phased basis-ket image from localWeylMonomial_basisKet, applies scaled_basisKet_inner, cancels the conjugate phase pair with I_pow_star_mul_self, and obtains 1. It finishes by rewriting the outer sum as Fin.sum_univ_four, instantiating the auxiliary claim four times, and simplifying with norm_num.
why it matters
The result supplies the squared norm of each local Weyl monomial, allowing them to be treated as an orthogonal (up to scaling) basis for the 4-by-4 operator space on a single core. It directly supports norm control when coupling cores and when building the discrete operator algebra that underlies the eight-tick octave in the forcing chain. No downstream theorems are listed, so the lemma functions as a normalization primitive for later global constructions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.