Documentation

CsdLean4.Mathlib.QuantumInfo.Register

Computational-basis register (R1 foundation) #

Category: 1-Mathlib (CSD-free; staged as a Mathlib-upstream candidate).

The foundation for the quantum-algorithm branch (specs/nqubit-register-plan.md). A register state over a finite computational basis ι is a vector in EuclideanSpace ℂ ι; the n-qubit register is the instance where the basis is the bitstrings:

QReg n := EuclideanSpace ℂ (Fin n → Fin 2).

This file provides the computational basis basisState, the Born probability prob, the coordinate-of-a-sum bridge sum_coord, and the core API: Born as a squared inner product (prob_eq_inner_sq), normalisation of a unit state (sum_prob_eq_one), and that a basis state is measured with certainty (prob_basisState). Downstream files add the Hadamard transform, the QFT (Fourier.lean), phase estimation (PhaseEstimation.lean), oracles, and the algorithms.

Generalised 2026-08-29 (a strict widening, at the second consumer per CONVENTIONS.md §9): the primitives were stated for bitstrings only, and Empirical/QM/Algorithms/ShorCore.lean carried a verbatim second copy over a general finite index for its ZMod N and Fin T registers. The general form subsumes both; the bitstring statements are the ι = Fin n → Fin 2 instances and every consumer elaborates as before.

source
@[reducible, inline]
abbrev QuantumInfo.QReg (n : ℕ) :
Type

An n-qubit register state: a vector in the 2ⁿ-dimensional Hilbert space indexed by bitstrings Fin n → Fin 2. The bitstring instance of the general finite-basis register below.

Equations
Instances For
    source
    noncomputable def QuantumInfo.basisState {ι : Type u_1} [DecidableEq ι] (x : ι) :
    EuclideanSpace ℂ ι

    The computational basis state |x⟩ indexed by an arbitrary finite type.

    Equations
    Instances For
      source
      @[simp]
      theorem QuantumInfo.basisState_apply {ι : Type u_1} [DecidableEq ι] (x y : ι) :
      (basisState x).ofLp y = if y = x then 1 else 0
      source
      noncomputable def QuantumInfo.prob {ι : Type u_1} (ψ : EuclideanSpace ℂ ι) (z : ι) :
      ℝ

      The Born probability of measuring computational-basis outcome z in state ψ: ‖ψ z‖² = ‖⟨z|ψ⟩‖².

      Equations
      Instances For
        source
        theorem QuantumInfo.prob_nonneg {ι : Type u_1} (ψ : EuclideanSpace ℂ ι) (z : ι) :
        0 ≤ prob ψ z
        source
        theorem QuantumInfo.prob_eq_inner_sq {ι : Type u_1} [DecidableEq ι] [Fintype ι] (ψ : EuclideanSpace ℂ ι) (z : ι) :
        prob ψ z = ‖inner ℂ (basisState z) ψ‖ ^ 2

        Born rule, inner-product form: the probability is the squared modulus of the amplitude ⟨z|ψ⟩.

        source
        theorem QuantumInfo.normSq_eq_sum_prob {ι : Type u_1} [Fintype ι] (ψ : EuclideanSpace ℂ ι) :
        ‖ψ‖ ^ 2 = ∑ z : ι, prob ψ z

        ‖v‖² = ∑ z, ‖v z‖² on the register (Parseval in coordinate form).

        source
        theorem QuantumInfo.sum_prob_eq_one {ι : Type u_1} [Fintype ι] {ψ : EuclideanSpace ℂ ι} (hψ : ‖ψ‖ = 1) :
        ∑ z : ι, prob ψ z = 1

        Normalisation: the Born probabilities of a unit register state sum to one.

        source
        @[simp]
        theorem QuantumInfo.basisState_norm {ι : Type u_1} [DecidableEq ι] [Fintype ι] (x : ι) :
        ‖basisState x‖ = 1
        source
        @[simp]
        theorem QuantumInfo.prob_basisState {ι : Type u_1} [DecidableEq ι] (x z : ι) :
        prob (basisState x) z = if z = x then 1 else 0

        A computational basis state is measured with certainty: prob |x⟩ z = [z = x].

        source
        theorem QuantumInfo.sum_coord {ι : Type u_1} {κ : Type u_2} (s : Finset κ) (f : κ → EuclideanSpace ℂ ι) (y : ι) :
        (∑ k ∈ s, f k).ofLp y = ∑ k ∈ s, (f k).ofLp y

        Coordinatewise: a finite sum of register states evaluates as the sum of coordinates.

        Coordinates of the inner product #

        normSq_eq_sum_prob above is the diagonal case of inner_eq_sum, which was missing: two protocol files each carried a copy (BACKLOG #146 cluster (C)). Both lemmas here are convenience specialisations, not library additions — inner_eq_sum is PiLp.inner_apply with the ℂ coordinate inner product unfolded, and mul_conj_eq is Complex.mul_conj carrying the norm-squared cast rather than normSq. The cast form is the reason to have the second one at all: the Born sums downstream need ((‖z‖ ^ 2 : ℝ) : ℂ) as the atom, so that Complex.ofReal_sum and friends fire.

        source
        theorem QuantumInfo.inner_eq_sum {ι : Type u_1} [Fintype ι] (x y : EuclideanSpace ℂ ι) :
        inner ℂ x y = ∑ i : ι, (starRingEnd ((fun (x : ι) => ℂ) i)) (x.ofLp i) * y.ofLp i

        The Euclidean inner product in coordinates: ⟨x,y⟩ = ∑ i, conj (x i) · y i.

        source
        theorem QuantumInfo.mul_conj_eq (z : ℂ) :
        z * (starRingEnd ℂ) z = ↑(‖z‖ ^ 2)

        z · conj z = ‖z‖² (the Complex.ofReal form, used to keep the cast atom canonical).