basisKet_orthonormal
plain-language theorem explainer
The standard ququart basis kets satisfy orthonormality under the explicit finite sum inner product. Researchers modeling finite-dimensional quantum structures within Recognition Science cite this to anchor the Hilbert space inner product for four-level states. The proof proceeds by exhaustive case split on the two Fin 4 indices followed by direct simplification against the basis definition.
Claim. For indices $m,n$ in the set of four elements, the standard basis vectors obey $∑_{t} ¯ψ_m(t) ψ_n(t) = δ_{mn}$, where ψ_k(t) equals 1 when t equals k and 0 otherwise.
background
The CoupledRecognitionCores module defines ququart states as maps from Fin 4 to ℂ. The basisKet construction supplies the standard basis vector with a unit entry at index m and zeros elsewhere. This theorem confirms that the finite-sum inner product recovers the Kronecker delta. It rests directly on the basisKet definition supplied in the same module and its alias in the OperatorCore submodule.
proof idea
The term-mode proof applies fin_cases to both m and n, generating all sixteen index pairs, then invokes simp with the basisKet definition to evaluate each sum to either 1 or 0.
why it matters
Orthonormality supplies the inner-product axiom used by the downstream scaled_basisKet_inner lemma, which lifts the result to linear combinations. The result therefore grounds the finite-dimensional operator algebra required for Recognition Science models that embed ququart representations. It closes the basic Hilbert-space setup before any dynamics or measurement postulates are introduced.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.