coupledBasisKet_orthonormal
plain-language theorem explainer
The theorem establishes orthonormality of the coupled basis kets under the finite-sum inner product over the ququart configuration space. Researchers constructing discrete Hilbert spaces for coupled recognition models cite it when evaluating inner products of basis states. The proof splits on index equality, rewrites the sum via the explicit indicator definition, and applies Finset.sum_eq_single or sum_eq_zero with case analysis on the summation variable.
Claim. Let $I_N = Fin N → Fin 4$ be the space of coupled core indices. For the standard basis vectors $e_s, e_t : I_N → ℂ$ given by $e_s(u) = 1$ if $u = s$ and $0$ otherwise, the sum satisfies $∑_{u ∈ I_N} conj(e_s(u)) · e_t(u) = δ_{st}$.
background
CoupledCoreIndex N is the finite set of all maps from Fin N to Fin 4, representing configurations of N coupled ququart cores. The function coupledBasisKet s is the indicator vector that equals 1 at index s and 0 elsewhere, supplying the concrete Hilbert carrier for these configurations.
proof idea
The proof performs by_cases on s = t. When equal, it rewrites the sum to the squared-norm form using the basis definition, then invokes Finset.sum_eq_single to isolate the diagonal term and simp to evaluate. When unequal, it applies Finset.sum_eq_zero and branches on whether the summation index u matches s or t, using the zero values from the definition to obtain the result.
why it matters
This orthonormality supplies the inner-product rule required by the downstream scaled_coupledBasisKet_inner lemma that extends the identity to linear combinations. It completes the orthonormal basis construction for the finite coupled-core space inside the foundation module, a prerequisite for operator algebras in the Recognition Science framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.