coupledOperatorInner
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.
claimFor 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 in Recognition Science
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.
scope and limits
- Does not extend beyond finite N.
- Does not incorporate the J-cost function or defect distances.
- Does not assume any particular form for the operators A and B.
- Does not interact with the phi-ladder mass formulas.
formal statement (Lean)
462def coupledOperatorInner {N : ℕ}
463 (A B : CoupledCoreSpace N →ₗ[ℂ] CoupledCoreSpace N) : ℂ :=
proof body
Definition body.
464 ∑ s : CoupledCoreIndex N, ∑ t : CoupledCoreIndex N,
465 star (A (coupledBasisKet s) t) * B (coupledBasisKet s) t
466
467/-- The coupled phase character has unit modulus. -/