coupledOperatorInner
plain-language theorem explainer
The definition coupledOperatorInner equips the space of linear operators on N coupled recognition cores with a Hilbert-Schmidt inner product. It is referenced in subsequent theorems that verify the norm and mutual orthogonality of tensor-Weyl monomials. The construction reduces to a double summation of conjugated matrix elements in the standard basis of the finite-dimensional carrier space.
Claim. For linear operators $A, B$ on the Hilbert space of $N$ coupled cores, the inner product is defined by the double sum $⟨A, B⟩ = ∑_{s,t ∈ I_N} ¯(A e_s)_t (B e_s)_t$, where $I_N$ indexes the configurations of $N$ ququarts and $e_s$ is the standard basis vector at configuration $s$.
background
CoupledCoreSpace N is the Hilbert space ℂ^{4^N} consisting of all functions from the index set CoupledCoreIndex N to ℂ. The index set itself is the set of all functions Fin N → Fin 4. The standard basis vector at index s is the function that takes value 1 at s and 0 at all other indices. This definition appears in the CoupledRecognitionCores module, which develops algebraic structures for these finite coupled systems as part of the Recognition Science foundation. It supplies the pairing that turns the operator space into a Hilbert space, drawing on the finite basis construction from the same module.
proof idea
As a definition, it directly translates the Hilbert-Schmidt pairing into a double sum over the finite set of indices. The expression extracts the t-component of A applied to the basis vector at s, conjugates it, multiplies by the corresponding component of B, and sums over all s and t. The implementation relies only on the summation primitives for finite types and the definition of the basis vectors.
why it matters
The definition is called by tensorWeylMonomial_self_inner to establish that each tensor-Weyl monomial has Hilbert-Schmidt norm squared equal to the carrier dimension, and by tensorWeylMonomial_shift_orthogonal to prove that distinct monomials are orthogonal. It thereby supports the construction of an orthonormal operator basis aligned with the eight-tick structure in the Recognition Science framework. No open scaffolding remains at this step.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.