tensorWeylMonomial_shift_orthogonal
plain-language theorem explainer
Distinct displacement labels a ≠ a' in the coupled ququart configuration space produce tensor-Weyl monomial operators that are orthogonal under the Hilbert-Schmidt inner product. Modelers of multi-core recognition systems cite this to guarantee an orthogonal operator family before constructing bases or dynamics. The proof is a one-line wrapper that unfolds the inner product and applies the per-basis-state image orthogonality theorem to each term in the resulting sum.
Claim. Let $N$ be a natural number and let $a,a'$ be distinct elements of the configuration space $C_N = (Fin N) → (Fin 4)$. For arbitrary $b,b' ∈ C_N$, the Hilbert-Schmidt pairing of the operators $T_{a,b}$ and $T_{a',b'}$ vanishes, where $T_{a,b}$ is the linear map that multiplies by the phase character of $b$ and shifts configurations by $a$, and the pairing is the sum over all pairs of configurations $s,t$ of the conjugated matrix element of the first operator times the matrix element of the second.
background
CoupledCoreIndex N is the finite configuration space of N coupled ququart cores, realized as maps Fin N → Fin 4. The tensorWeylMonomial a b is the operator on the coupled Hilbert space whose action on a state ψ at site s is the phaseCharacter b s times ψ evaluated at the configuration shifted by a. The coupledOperatorInner is the Hilbert-Schmidt pairing that sums, over all pairs s,t, the product of the conjugate of the first operator's matrix element and the second operator's matrix element at those indices.
proof idea
The term proof first unfolds the definition of coupledOperatorInner, exposing a double sum over configurations. It then applies Finset.sum_eq_zero and supplies the exact term tensorWeylMonomial_basis_image_orthogonal h b b' s for each summand, which is the upstream result establishing that the images of any fixed basis ket under the two monomials are orthogonal.
why it matters
The result guarantees that tensor-Weyl monomials labeled by distinct shifts a form an orthogonal set in the operator algebra of coupled recognition cores. It directly extends the basis-image orthogonality theorem and supplies a necessary algebraic step for any later construction of orthonormal bases or dynamics in the CoupledRecognitionCores layer. No downstream uses are recorded yet, but the statement closes the orthogonality requirement for the finite-N case before scaling arguments or phi-ladder embeddings are applied.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.