scaled_coupledBasisKet_inner
plain-language theorem explainer
The lemma computes the sesquilinear inner product of two scaled standard basis vectors in the finite-dimensional Hilbert space of N coupled ququart cores, returning the product of the complex scalings times the Kronecker delta on the indices. Workers constructing tensor-Weyl monomials or coupled operator cores cite it to verify orthogonality after displacement. The tactic proof expands the scalings via sum congruence and ring, factors the constant via mul_sum, then rewrites directly with the unscaled orthonormality result.
Claim. Let $c,d$ be complex scalars and $m,n$ indices in the configuration space $CoupledCoreIndex(N) := Fin N → Fin 4$. Then $∑_t star((c · ψ_m(t))) · (d · ψ_n(t)) = star c · d · (1 if m=n else 0), where ψ_k is the standard basis vector with ψ_k(t) = 1 precisely when t = k.
background
CoupledCoreIndex(N) is the finite configuration space Fin N → Fin 4 that labels the concrete Hilbert carrier of N coupled recognition cores. The function coupledBasisKet(s) returns the standard basis vector that equals 1 at site s and 0 elsewhere. Its orthonormality theorem states that the explicit finite sum over u of star(coupledBasisKet s u) times coupledBasisKet t u equals 1 if s = t and 0 otherwise.
proof idea
The calc block first applies Finset.sum_congr with Pi.smul_apply and ring to pull star c * d out of each term. It then rewrites the constant factor outside the sum via Finset.mul_sum. The final step invokes the upstream theorem coupledBasisKet_orthonormal to replace the remaining sum by the Kronecker delta.
why it matters
This result supplies the scaled inner-product rule required by the two downstream theorems tensorWeylMonomial_basis_image_orthogonal and tensorWeylMonomial_self_inner. Those theorems establish orthogonality of distinct tensor-Weyl displacements and the Hilbert-Schmidt norm of each monomial, both of which sit inside the operator-core layer that supports the Recognition Composition Law and the eight-tick octave structure.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.