Qubit states

An n-qubit pure state is a unit vector in ℂ^(2^n) with the L2 inner product. The raw Hilbert-space vector type is StateVector n; PureState n bundles such a vector with its unit-norm proof.

Naming: PureState, not State

In quantum mechanics the general notion of a state is a density operator (density matrix); pure states are the special case of a closed system with maximal knowledge. The algorithms in this library live entirely in that special case (pure state + unitary evolution + projective measurement), but the library does not redefine the standard term: this type is PureState, and the bare name State is deliberately left undefined, reserved for the density-operator concept should the library later introduce mixed states (a pure state then embeds as the rank-one projector |ψ⟩⟨ψ|).

Conventions

• Endianness: computational basis states of an n-qubit register are labelled by n-bit strings read as integers 0, …, 2^n - 1 [dW19, qcnotes.tex:587], leftmost bit most significant. We index qubits left to right, so the basis label x : Fin (2 ^ n) encodes |q₀ q₁ … q_{n-1}⟩ with x = Σ qᵢ · 2^(n-1-i): qubit 0 carries the most significant bit.
• Normalization is part of PureState: every value carries a proof that its underlying vector has norm 1. Linear combinations live at the raw StateVector layer until separately proved normalized.
• Components are accessed by plain application ψ i; the underlying vector of ψ : PureState n is (ψ : StateVector n).

Main definitions

• LeanPool.LeanQuantumAlg.StateVector n — the Hilbert-space vector type EuclideanSpace ℂ (Fin (2 ^ n)).
• LeanPool.LeanQuantumAlg.PureState n — unit vectors in StateVector n.
• LeanPool.LeanQuantumAlg.PureState.ket x — computational basis ket |x⟩ (PiLp.single 2 x 1).

The named one-qubit kets (ket0, ket1, ketPlus, ketMinus) and the scalar invSqrt2 now live in LeanPool.LeanQuantumAlg.Core.Components.Kets.

Pinned Mathlib API: PiLp.single, PiLp.single_apply, PiLp.norm_single, EuclideanSpace.norm_eq.

@[reducible, inline]

abbrev QuantumAlg.StateVector (n : ℕ) : Type

Raw Hilbert-space vector for an n-qubit pure-state register.

Equations

• QuantumAlg.StateVector n = EuclideanSpace ℂ (Fin (2 ^ n))

structure QuantumAlg.PureState (n : ℕ) : Type

An n-qubit pure state: a unit vector in the computational Hilbert space.

The general (density-operator) notion of state is intentionally not defined here — see the module docstring.

• vec : StateVector n

  Underlying Hilbert-space vector.

• norm_eq_one : ‖self.vec‖ = 1

  Pure states are normalized by definition.

@[implicit_reducible]

instance QuantumAlg.PureState.instCoeStateVector {n : ℕ} : Coe (PureState n) (StateVector n)

Equations

• QuantumAlg.PureState.instCoeStateVector = { coe := QuantumAlg.PureState.vec }

@[implicit_reducible]

instance QuantumAlg.PureState.instCoeFunForallFinHPowNatOfNatComplex {n : ℕ} : CoeFun (PureState n) fun (x : PureState n) => Fin (2 ^ n) → ℂ

Equations

• QuantumAlg.PureState.instCoeFunForallFinHPowNatOfNatComplex = { coe := fun (ψ : QuantumAlg.PureState n) => ψ.vec.ofLp }

@[implicit_reducible]

noncomputable instance QuantumAlg.PureState.instNorm {n : ℕ} : Norm (PureState n)

Equations

• QuantumAlg.PureState.instNorm = { norm := fun (ψ : QuantumAlg.PureState n) => ‖ψ.vec‖ }

@[implicit_reducible]

noncomputable instance QuantumAlg.PureState.instInnerComplex {n : ℕ} : Inner ℂ (PureState n)

Equations

• QuantumAlg.PureState.instInnerComplex = { inner := fun (ψ φ : QuantumAlg.PureState n) => inner ℂ ψ.vec φ.vec }

@[implicit_reducible]

instance QuantumAlg.PureState.instHAddStateVector {n : ℕ} : HAdd (PureState n) (PureState n) (StateVector n)

Equations

• QuantumAlg.PureState.instHAddStateVector = { hAdd := fun (ψ φ : QuantumAlg.PureState n) => ψ.vec + φ.vec }

@[implicit_reducible]

instance QuantumAlg.PureState.instHSubStateVector {n : ℕ} : HSub (PureState n) (PureState n) (StateVector n)

Equations

• QuantumAlg.PureState.instHSubStateVector = { hSub := fun (ψ φ : QuantumAlg.PureState n) => ψ.vec - φ.vec }

@[implicit_reducible]

instance QuantumAlg.PureState.instHSMulComplexStateVector {n : ℕ} : HSMul ℂ (PureState n) (StateVector n)

Equations

• QuantumAlg.PureState.instHSMulComplexStateVector = { hSMul := fun (c : ℂ) (ψ : QuantumAlg.PureState n) => c • ψ.vec }

@[simp]

theorem QuantumAlg.PureState.hAdd_apply {n : ℕ} (ψ φ : PureState n) (i : Fin (2 ^ n)) : (ψ.vec + φ.vec).ofLp i = ψ.vec.ofLp i + φ.vec.ofLp i

@[simp]

theorem QuantumAlg.PureState.hSub_apply {n : ℕ} (ψ φ : PureState n) (i : Fin (2 ^ n)) : (ψ.vec - φ.vec).ofLp i = ψ.vec.ofLp i - φ.vec.ofLp i

@[simp]

theorem QuantumAlg.PureState.hSMul_apply {n : ℕ} (c : ℂ) (ψ : PureState n) (i : Fin (2 ^ n)) : (c • ψ.vec).ofLp i = c * ψ.vec.ofLp i

def QuantumAlg.PureState.ofVec {n : ℕ} (v : StateVector n) (h : ‖v‖ = 1) : PureState n

Build a pure state from a normalized Hilbert-space vector.

Equations

• QuantumAlg.PureState.ofVec v h = { vec := v, norm_eq_one := h }

@[simp]

theorem QuantumAlg.PureState.coe_ofVec {n : ℕ} (v : StateVector n) (h : ‖v‖ = 1) : (ofVec v h).vec = v

@[simp]

theorem QuantumAlg.PureState.ofVec_apply {n : ℕ} (v : StateVector n) (h : ‖v‖ = 1) (i : Fin (2 ^ n)) : (ofVec v h).vec.ofLp i = v.ofLp i

@[simp]

theorem QuantumAlg.PureState.norm_eq_one' {n : ℕ} (ψ : PureState n) : ‖ψ.vec‖ = 1

theorem QuantumAlg.PureState.ext {n : ℕ} {ψ φ : PureState n} (h : ∀ (i : Fin (2 ^ n)), ψ.vec.ofLp i = φ.vec.ofLp i) : ψ = φ

theorem QuantumAlg.PureState.ext_iff {n : ℕ} {ψ φ : PureState n} : ψ = φ ↔ ∀ (i : Fin (2 ^ n)), ψ.vec.ofLp i = φ.vec.ofLp i

def QuantumAlg.PureState.ket {n : ℕ} (x : Fin (2 ^ n)) : PureState n

The computational basis ket |x⟩ : PureState n, big-endian (qubit 0 is the most significant bit of x).

Equations

• QuantumAlg.PureState.ket x = QuantumAlg.PureState.ofVec (PiLp.single 2 x 1) ⋯

@[simp]

theorem QuantumAlg.PureState.ket_apply {n : ℕ} (x i : Fin (2 ^ n)) : (ket x).vec.ofLp i = if i = x then 1 else 0

theorem QuantumAlg.PureState.ket_injective {n : ℕ} : Function.Injective ket

theorem QuantumAlg.PureState.norm_ket {n : ℕ} (x : Fin (2 ^ n)) : ‖(ket x).vec‖ = 1