QuantumComputinglib learn · inspect · formalize
Checked on this commit 4,524 public declarations commit c681192368c2 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>H●measurement
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.

New to quantum computing? Start here.

What a quantum computer is doing in this book

A classical program updates bits. In the circuit model used here, a quantum program applies reversible linear transformations to complex amplitude vectors and reads classical outcomes through measurement.

\[|\psi\rangle=\alpha|0\rangle+\beta|1\rangle,\qquad |\alpha|^2+|\beta|^2=1\]
\[P(x)=|\langle x|\psi\rangle|^2\]
A first two-qubit circuit: H creates a superposition and CNOT turns it into an entangled Bell pair.
q0 |0> Hcontrol Bell pair
q1 |0> X target Bell pair
\[|\Phi^+\rangle=(|00\rangle+|11\rangle)/\sqrt2\]
  1. StateDescribe the information by complex amplitudes.
  2. GateApply a unitary matrix; this is the reversible evolution step.
  3. CircuitCompose gates from left to right in time.
  4. MeasurementConvert amplitudes into classical outcome probabilities.
  5. ASPBEUse those ingredients to prepare useful states and embed useful non-unitary matrices into unitaries.
How to read this site. Read the circuit picture first, switch to Math when the notation feels familiar, and switch to Lean only when you want the machine-checked statement.

Textbook / teaching anchor

Quantum Computer Science

N. David Mermin

Circuit-first computer-science viewpoint on qubits and quantum information.

Textbook / teaching anchor

Basics of quantum information

IBM Quantum Learning / John Watrous

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

Guided reading

Current book: two parts, one shared Lean graph

Part I develops State Preparation after the shared finite-matrix and circuit foundations. Part II develops Block Encoding on exactly those same lower nodes. The intended inclusion-like curriculum direction is Part I → Part II: a verified PREPARE is a reusable subproblem inside many block-encoding constructions. A block can also be consumed for state preparation, but that is a different downstream theorem requiring input, accepted-branch, normalization and success-cost obligations.

Reading map

Nested preparation layer, explicit transport hypotheses

The graph makes State Preparation a reusable subproblem of the broader Block Encoding toolchain without identifying their certificate types. Reverse block-to-state consumption remains a separately typed path.

Shared foundations and typed SP/BE bridges editable Mermaid source
flowchart TB
  F["Shared foundations<br/>finite matrices, basis states, circuits"]

  F --> S1["State preparation"]
  S1 --> S2["State action and<br/>first-column certificates"]
  S2 --> S3["Prepared-state routes<br/>and reusable PREPARE components"]

  F --> B1["Block encoding"]
  B1 --> B2["Ancillas, register order,<br/>normalization and projection"]
  B2 --> B3["Composition, dilation,<br/>LCU and QSVT interfaces"]

  S3 -. "nested PREPARE layer + SELECT + unprepare" .-> B3
  B3 -. "downstream consumer only: input + branch + normalization/amplification" .-> S3
  S3 --> H["ASPBE search,<br/>verification and exports"]
  B3 --> H

  classDef shared fill:#f8f5ee,stroke:#826a32,color:#222222,stroke-width:1.5px;
  classDef state fill:#edf5f1,stroke:#2f7355,color:#18382b,stroke-width:1.5px;
  classDef block fill:#eef3f7,stroke:#49677d,color:#1f2e39,stroke-width:1.5px;
  classDef system fill:#ffffff,stroke:#64747a,color:#222222,stroke-width:1.25px;
  class F shared;
  class S1,S2,S3 state;
  class B1,B2,B3 block;
  class H system;

Current chapters

Part I · State Preparation / Part II · Block Encoding

Part I · State Preparation

Chapters 1–2 are shared foundations authored once and reused by Block Encoding; Chapters 3–4 specialize them to preparation certificates.

Part II · Block Encoding

Block Encoding reuses the same finite-matrix and circuit nodes, then adds projected-block, composition, resource and proof-gated construction obligations.

Planned curriculum · not current theorem status

Future Quantum Information and Quantum Scientific Computing

New chapters must reuse compatible lower graph nodes and pass the same source, semantic, Lean, integration, exposition and independent-review gates. A source listed here is a curriculum anchor, not a claim of formalization.

Conceptual curriculum roadmap; dashed transports are not Lean implications editable Mermaid source
flowchart TB
  CORE["Shared Lean graph<br/>finite linear algebra · tensors · registers · unitaries<br/>states/density operators · channels · norms/distances · resources"]

  subgraph CURRENT["Current textbook"]
    SP["Part I · State Preparation<br/>U|0^n⟩ = |ψ⟩"]
    BE["Part II · Block Encoding<br/>‖A - αΠUΠ†‖ ≤ ε"]
  end

  QIT["Planned Part III · Quantum Information<br/>Leditzky: symmetry · Schur–Weyl · de Finetti<br/>cloning · spectrum estimation"]
  SCI["Planned Part IV · Quantum Scientific Computing<br/>Lin–Wiebe: QSP/QSVT · simulation · QPE<br/>walks · linear systems/ODEs · open systems"]

  EXT["Attributed external Lean references<br/>Mathlib · quantum-computing-lean · Lean-QuantumInfo<br/>lean-quantum · Lean-QuantumAlg-Bench · Lean-QIT-Bench"]

  CORE --> SP
  CORE --> BE
  CORE --> QIT
  CORE --> SCI
  SP -. "nested preparation layer + SELECT + unprepare" .-> BE
  BE -. "downstream consumer (not inclusion): input + branch + normalization/amplification" .-> SP
  BE --> SCI
  QIT --> SCI
  EXT -. "reviewed reuse / narrow adapters only" .-> CORE

  NOTE["Conceptual curriculum graph only.<br/>Dashed arrows are conditional transports, not Lean implications."]
  NOTE -.-> CURRENT
  NOTE -.-> QIT
  NOTE -.-> SCI

  classDef core fill:#f8f5ee,stroke:#826a32,color:#222222,stroke-width:1.5px;
  classDef state fill:#edf5f1,stroke:#2f7355,color:#18382b,stroke-width:1.5px;
  classDef block fill:#eef3f7,stroke:#49677d,color:#1f2e39,stroke-width:1.5px;
  classDef future fill:#f7f4fb,stroke:#735a8f,color:#2f2440,stroke-width:1.5px;
  classDef external fill:#ffffff,stroke:#64747a,color:#222222,stroke-width:1.25px;
  class CORE core;
  class SP state;
  class BE block;
  class QIT,SCI future;
  class EXT,NOTE external;

Planned Part III

Quantum Information and symmetry

Leditzky's representation-theoretic QIT notes anchor density operators/measurements, composite systems and entanglement, representation theory, Schur–Weyl duality, invariant states, de Finetti, cloning and spectrum-estimation routes.

Planned Part IV

Quantum algorithms for scientific computation

Lin–Wiebe, 29 April 2026 anchors channels/distances, query models, perturbation/statistics, qubitization/QSP/QSVT, simulation, phase estimation, walks, linear systems, differential equations and open systems. Its Block Encoding chapter reuses Part II rather than creating a second API.

Source policy. The 29 April Lin–Wiebe edition supplied to the project is publicly hosted by the authors, so the repository records the public source rather than vendoring a large PDF. A genuinely non-public appendix may be stored later only with provenance and reuse/license review.