innerProduct
plain-language theorem explainer
The definition supplies the standard Hermitian inner product on finite-dimensional complex vectors for quantum states in the ledger model. Quantum information researchers cite it when showing that unitary cloning would violate inner-product preservation. It is introduced directly as the sum of conjugate amplitudes times amplitudes over the basis.
Claim. For normalized states represented by amplitude vectors in dimension $n$, the inner product is defined by $⟨ψ|φ⟩ := ∑_{i=0}^{n-1} conj(ψ_i) φ_i$.
background
In the Information.NoCloning module, a QuantumState n is a structure holding amplitudes : Fin n → ℂ together with the normalization condition that the sum of squared moduli equals 1. This representation is drawn from the upstream QuantumState in QuantumLedger, where states appear as superpositions over ledger configurations with the same amplitude and normalization data. The module's setting derives the no-cloning theorem from ledger uniqueness: any attempt to duplicate an unknown state would require a balancing entry that cannot exist without prior knowledge of the amplitudes.
proof idea
Direct definition that implements the Hermitian inner product by summing the product of the complex conjugate of the first state's amplitudes with the second state's amplitudes over Finset.univ.
why it matters
The definition is used by the downstream theorem inner_product_self, which proves that the modulus of the self-inner-product equals 1, and appears as a constructor in the LinearAlgebraOp inductive type. It fills the algebraic step in the module's derivation of no-cloning from ledger uniqueness, where inner-product preservation under unitary maps is required to reach the contradiction ⟨ψ|φ⟩² ≠ ⟨ψ|φ⟩ for distinct states.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.