innerProduct
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.
claimFor 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 in Recognition Science
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.
scope and limits
- Does not extend to infinite-dimensional Hilbert spaces.
- Does not include Dirac bra-ket notation.
- Does not prove linearity or conjugate symmetry.
- Does not address continuous spectra or unbounded operators.
Lean usage
theorem norm_one {n} (ψ : QuantumState n) : ‖innerProduct ψ ψ‖ = 1 := inner_product_self ψformal statement (Lean)
55noncomputable def innerProduct {n : ℕ} (ψ φ : QuantumState n) : ℂ :=
proof body
Definition body.
56 Finset.univ.sum fun i => (starRingEnd ℂ) (ψ.amplitudes i) * φ.amplitudes i
57
58/-- **THEOREM**: Inner product with self equals 1. -/