scaled_basisKet_inner
plain-language theorem explainer
Scaled basis kets in the ququart space obey the sesquilinear inner product formula that factors out the complex scalars and inserts the Kronecker delta on the indices. Workers on discrete operator algebras and Weyl systems in four dimensions cite this when deriving orthogonality for monomial families. The proof expands the definition of scalar multiplication on the vectors, factors the resulting constant, and reduces the remaining sum via the orthonormality theorem for the basis.
Claim. For complex scalars $c,d$ and indices $m,n$ in the set of four elements, the inner product of the scaled standard basis vectors $c|m⟩$ and $d|n⟩$ equals $¯c d$ if $m=n$ and zero otherwise, where the inner product is the sum over the four components of the conjugate of the first vector times the second.
background
The CoupledRecognitionCores module works in a four-dimensional Hilbert space whose vectors are maps from the finite index set of four elements to the complex numbers. The standard basis ket for index $m$ is the vector that equals one at position $m$ and zero elsewhere. This construction supplies the concrete vectors needed to define local Weyl monomials that carry shift and phase labels.
proof idea
The proof is a calc chain. It first applies sum congruence and simplification with the scalar-multiplication rule on functions together with ring arithmetic to pull the scalars outside the sum. The constant factor is then moved in front via the sum-multiplication identity. The remaining sum is replaced by the Kronecker delta using the upstream orthonormality theorem for the unscaled basis vectors.
why it matters
The lemma supplies the algebraic identity required to evaluate Hilbert-Schmidt inner products of local Weyl monomials in the three downstream theorems on self-norm and orthogonality under mismatched phase or shift labels. It thereby supports the operator-core layer that realizes discrete representations inside the Recognition Science foundation. The step is consistent with the eight-tick octave structure of the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.