localWeylMonomial_orthogonal_of_ne
plain-language theorem explainer
Distinct local Weyl monomials on a single ququart core are orthogonal under the Hilbert-Schmidt inner product. Researchers building finite operator bases for single-core Recognition models cite this to confirm the 16-element family behaves as an orthogonal set. The proof splits on equality of the shift indices and routes to the phase or shift orthogonality lemmas.
Claim. Let $W_{a,b}$ be the local Weyl monomial operator on the ququart space. If $(a,b) ≠ (a',b')$ for $a,b,a',b' ∈ {0,1,2,3}$, then the Hilbert-Schmidt inner product of $W_{a,b}$ and $W_{a',b'}$ equals zero.
background
The local Weyl monomial is the operator $W_{a,b}$ acting on ququart states by $W_{a,b} ψ(s) = i^{b·s} ψ(s-a)$, where subtraction uses the mod-4 group law on Fin 4. The inner product is the Hilbert-Schmidt pairing that sums the conjugate product of matrix elements over the standard orthonormal ququart basis. This theorem sits inside the CoupledRecognitionCores module, which assembles single-core operators before coupling them across cores.
proof idea
The tactic proof performs case analysis on whether the shift indices a and a' coincide. When they match, it substitutes and invokes the phase orthogonality lemma after deriving a contradiction on the phase indices from the distinct-pair hypothesis. When they differ, it applies the shift orthogonality lemma directly.
why it matters
The result supplies the missing case that completes full orthogonality for all distinct one-core Weyl labels, a prerequisite for treating the family as an orthogonal operator basis in single-core decompositions. It feeds the construction of the 16-element Weyl set whose cardinality is noted in the immediately following comment. No downstream theorems are recorded yet, leaving its use in larger Recognition chains open.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.