QuantumComputinglib learn · inspect · formalize
Checked on this commit 2,822 public declarations commit 07559c3d051f Build record

Foundation lesson · do not skip this if you are new

Before the cases: how a quantum algorithm gets access to data and matrices

A quantum algorithm is not given a NumPy array for free. Before discussing speedups, we must say how classical data, matrix entries, or a linear operator become quantum operations. State preparation, query oracles, and block encodings are three different access contracts.

State preparation

\[P|0^n\rangle=|\psi\rangle\]

Contract. Build a circuit P that creates the input quantum state you actually want to use.

Why it matters. Algorithms that start from amplitude-encoded data need this state before any later quantum subroutine can help. Preparation cost is therefore part of the end-to-end algorithm, not decorative preprocessing.

The Pauli-X and Hadamard cases show the smallest exact examples.

Digital query oracle

\[O_H|i\rangle|j\rangle|0\rangle=|i\rangle|j\rangle|H_{ij}\rangle\]

Contract. Ask a reversible black box for a matrix entry encoded in a work register.

Why it matters. Query-complexity theorems often count how many times the oracle is called, but a real fault-tolerant implementation must also build the arithmetic and memory circuit hidden inside that call.

The GHL Robin paper explicitly contrasts this model with its gate-level construction.

Block encoding

\[(\langle0^a|\otimes I)U_A(|0^a\rangle\otimes I)=A/\alpha\]

Contract. Embed a possibly non-unitary matrix A as the clean ancilla block of a larger unitary U_A.

Why it matters. Quantum hardware applies unitary gates. Block encoding is the interface that lets algorithms such as QSVT and Hamiltonian simulation manipulate a general structured matrix through a unitary circuit.

BE Case 1, the cubic diagonal family, and the Robin case all certify this contract.

How to read a quantum circuit

Follow the state from left to right

q0: |0>Hmeasurement
q1: |0>measurement
  • wireA horizontal wire is one qubit/register. Time flows from left to right.
  • |0>A ket at the left fixes the input state of that wire.
  • H, X, RYA box is a gate. Its matrix acts when the state reaches that box.
  • controlA control dot means another gate acts only when the control condition is satisfied.
  • daggerU† means the inverse/conjugate-transpose circuit; it often uncomputes temporary information.
  • ancillaAn ancilla is workspace. A clean block-encoding proof normally requires selected ancillas to start and end in |0>.
  • measurementMeasurement converts quantum amplitudes into classical outcomes; it is different from the coherent unitary part of the circuit.

The H-plus-CNOT circuit above prepares the Bell state \((|00\rangle+|11\rangle)/\sqrt2\). The same visual grammar is used in the case studies; larger diagrams only add named registers and uncomputation.

Reading mode Start visually; reveal formalism only when you want it.

Beginner layer · first ASPBE problem

State preparation asks: which circuit creates the vector I want?

You know the desired amplitudes. The construction problem is to find a unitary whose action on the easy input |0…0⟩ produces exactly those amplitudes.

The smallest nontrivial preparation: Hadamard creates |+⟩.
q₀ |0⟩ H |+⟩
  1. TargetWrite the normalized amplitude vector you want.
  2. CandidateChoose gates whose product might have that target as column zero.
  3. CheckProve the whole matrix is unitary, not only that one column looks right.
  4. CertifyProve the zero-input column equals the target exactly.

Textbook / teaching anchor

Basics of quantum information

IBM Quantum Learning / John Watrous

Beginner-friendly state-vector, measurement, multi-system, and circuit explanations.

Strict mathematics, after the picture

The equations behind the intuition

\[U|0^n\rangle=|\psi\rangle\]
\[H|0\rangle=\frac{|0\rangle+|1\rangle}{\sqrt2}\]
\[X|0\rangle=|1\rangle\]

Every symbol used here is connected below to a compiled declaration or a clearly marked research-source formula.

Textbook / teaching anchor

Basics of quantum information

IBM Quantum Learning / John Watrous

Beginner-friendly state-vector, measurement, multi-system, and circuit explanations.

Learn Lean while learning quantum computing

Lean idea: a certificate is a structure

structure ComplexStatePreparationCertificate where
  target
  gate
  normalizationProof
  preparationProof

The circuit, target, and proofs travel together. A downstream theorem cannot accidentally forget normalization or unitarity.

The full proof-backed declarations for this chapter are shown immediately below.

Application 1

State preparation

Given a normalized target \(|\psi\rangle\), construct a unitary \(U\) that sends the all-zero state to it. ASPBE treats this as its own synthesis and proof problem, with its own exact and approximate acceptance predicates.

\[U|0^n\rangle=|\psi\rangle\]

One qubit is enough to see the contract

Two familiar gates, two concrete targets

The Hadamard statement is correct: it prepares the equal superposition from \(|0\rangle\). Pauli \(X\) exchanges \(|0\rangle\) and \(|1\rangle\).

Hadamard prepares a superposition

\(H|0\rangle=(|0\rangle+|1\rangle)/\sqrt{2}\)

The two computational-basis amplitudes have equal magnitude.

Pauli X swaps the basis states

\(X|0\rangle=|1\rangle,\quad X|1\rangle=|0\rangle\)

This is a basis-state preparation, not an arbitrary superposition.

Independent proof route

What ASPBE has to establish

The target must be normalized. The proposed matrix must be unitary. Finally, its action on the zero ket, equivalently its first column, must match every target amplitude.

State-preparation proof and export flow editable Mermaid source
flowchart LR
  T["Target state<br/>|ψ⟩"] --> N["Check normalization<br/>⟨ψ|ψ⟩ = 1"]
  N --> C["Choose a circuit<br/>or unitary completion"]
  C --> U["Prove U is unitary"]
  C --> A["Prove the state action<br/>U|0ⁿ⟩ = |ψ⟩"]
  U --> L["Lean state-preparation<br/>certificate"]
  A --> L
  L --> E["Export one certified<br/>finite instance"]

  classDef target fill:#ffffff,stroke:#6b6045,color:#222222,stroke-width:1.5px;
  classDef work fill:#ffffff,stroke:#64747a,color:#222222,stroke-width:1.25px;
  classDef proof fill:#ffffff,stroke:#2f7355,color:#18382b,stroke-width:1.5px;
  class T,N target;
  class C,U,A work;
  class L,E proof;

Certificate anatomy

Three facts travel together

Normalized target
The requested amplitude vector has unit norm.
Unitary candidate
The circuit matrix preserves inner products, not merely the first column.
State action
Applying the candidate to \(|0^n\rangle\) returns the requested vector.

A preparation circuit may later become a PREPARE component in an LCU or purification construction. That downstream block-encoding theorem remains a separate proof obligation.

Continue reading

State-preparation chapters