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 |+⟩

TargetWrite the normalized amplitude vector you want.
CandidateChoose gates whose product might have that target as column zero.
CheckProve the whole matrix is unitary, not only that one column looks right.
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.

Textbook / teaching anchor

Quantum Computation lecture notes

John Preskill

Foundations, entanglement, circuits, algorithms, and error correction.

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.

Textbook / teaching anchor

Quantum Computation lecture notes

John Preskill

Foundations, entanglement, circuits, algorithms, and error correction.

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.

State preparation · Chapter 3 of 9

The state-preparation problem

Ask one concrete question: which unitary sends the all-zero basis state to the normalized state we want?

Lean modules used in this chapter

QuantumBlockEncoding/StatePreparation.lean
QuantumBlockEncoding/ConcreteSemantics.lean
QuantumBlockEncoding/TextbookStatePreparation.lean

Textbook lesson

Build the idea before opening the proof

State preparation asks for one observable action: start in the all-zero basis state and end at a specified normalized target.

The contract

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

The input is fixed, but U must still be a unitary on the whole 2^n-dimensional space. Specifying only the desired output vector is not yet a circuit.

Pauli X

\[X=\begin{pmatrix}0&1\\1&0\end{pmatrix},\qquad X|0\rangle=|1\rangle.\]

X exchanges the two computational-basis states. The formal example represents X as Mathlib's swap matrix and obtains unitarity from self-invertibility.

Hadamard

\[H=\frac1{\sqrt2}\begin{pmatrix}1&1\\1&-1\end{pmatrix},\qquad H|0\rangle=|+\rangle.\]

The plus state has two equal amplitudes. Lean separately proves the square-root normalization, H's unitary equation, and the zero-state action.

Check your understanding

Open both complete certificates below and identify the exact line that proves normalization, unitarity, and preparation.

Mathematical order and conventions adapted from Lin, Lecture Notes on Quantum Algorithms for Scientific Computation. The formal checkpoints and ASPBE status distinctions are specific to this library.

Route at a glance

Where these results sit

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;

Selected declarations

Read the mathematics beside the Lean statement

A compiled route means that the reusable theorem or constructor and at least one finite witness compile. Hardware- and problem-specific downstream instantiations are out of scope, not universal claims made by these cards.

Lean result

Hadamard prepares the plus state

QuantumBlockEncoding.TextbookStatePreparation.hadamardCertificate_prepares_plus

DeclarationCompiled Full routeCompiled

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

What it says

The standard Hadamard matrix is proved unitary and maps the zero ket to the normalized equal superposition.

Why it matters

The first column of H contains the two target amplitudes, both equal to one over square root two. This is the smallest complete example where normalization is genuinely more than a basis-vector check.

How the proof goes

Prove the square-root identity, check H times its conjugate transpose is identity, and identify column zero with the target vector.

Uses: QuantumBlockEncoding.TextbookStatePreparation.hadamard_unitary; QuantumBlockEncoding.TextbookStatePreparation.plusTarget_normalized
Still outside this result: None for this local declaration.

Route closure

QuantumBlockEncoding.TextbookStatePreparation.hadamardCertificate_prepares_plus

Natural-language steps and Lean objects

Mathematical step	Lean object or step
Prove the target has norm one.	`plusTarget_normalized`
Prove the matrix is unitary.	`hadamard_unitary`
Evaluate H on the zero ket.	`hadamard_prepares_plus`
Package all three facts.	`hadamardCertificate`

Open the Lean statement and source links

theorem hadamardCertificate_prepares_plus :
    applyVec hadamardCertificate.gate.matrix (zeroKet 1) =
      hadamardCertificate.target.amplitudes :=
  hadamardCertificate.preparesVector

Local declaration · Verso Blueprint · commit-pinned GitHub source

Lean result

Pauli X prepares the one state

QuantumBlockEncoding.TextbookStatePreparation.pauliXCertificate_prepares_one

DeclarationCompiled Full routeCompiled

X|0\rangle=|1\rangle,\qquad X|1\rangle=|0\rangle.

What it says

The Pauli X permutation is proved unitary and sends the zero basis state to the one basis state.

Why it matters

X swaps the two basis columns; selecting its first column therefore gives the one-state amplitudes. It gives beginners a complete certificate without irrational amplitudes or hidden analytic assumptions.

How the proof goes

Use Mathlib's swap matrix, its self-inverse theorem, and the basis-ket column-selection lemma.

Uses: QuantumBlockEncoding.TextbookStatePreparation.pauliX_unitary; QuantumBlockEncoding.TextbookStatePreparation.oneTarget_normalized
Still outside this result: None for this local declaration.

Route closure

QuantumBlockEncoding.TextbookStatePreparation.pauliXCertificate_prepares_one

Natural-language steps and Lean objects

Mathematical step	Lean object or step
Represent X as a swap matrix.	`pauliX`
Use self-inverse to prove unitarity.	`pauliX_unitary`
Select the zero-input column.	`pauliX_prepares_one`
Package the certificate and cost.	`pauliXVerified`

Open the Lean statement and source links

theorem pauliXCertificate_prepares_one :
    applyVec pauliXCertificate.gate.matrix (zeroKet 1) =
      pauliXCertificate.target.amplitudes :=
  pauliXCertificate.preparesVector

/-- The certified Hadamard example prepares the equal superposition. -/

Local declaration · Verso Blueprint · commit-pinned GitHub source

Lean result

The state-preparation contract

QuantumBlockEncoding.StatePreparationCandidate.preparesTarget

DeclarationCompiled Full routeCompiled

U\lvert 0^n\rangle=\lvert\psi\rangle.

What it says

The candidate unitary prepares the target from the zero basis state.

Why it matters

The target amplitudes are the first column of the unitary matrix. It gives state preparation its own acceptance test, independent of any later use in block encoding.

How the proof goes

Unfold the candidate action on the zero basis vector and compare every amplitude.

Uses: QuantumBlockEncoding.StatePreparationTarget; QuantumBlockEncoding.StatePreparationCandidate
Still outside this result: None within the declared reusable route.

Route closure

Natural-language steps and Lean objects

Mathematical step	Lean object or step
Select the all-zero input column.	`candidate.unitary row (zeroBasisIndex qubits)`
Match it with the requested amplitude.	`= candidate.target.amplitudes row`

Open the Lean statement and source links

def preparesTarget (candidate : StatePreparationCandidate α qubits) : Prop :=
  FirstColumnMatches candidate.unitary candidate.target

/-- Reuse the block-encoding resource order for state-preparation candidates. -/

Local declaration · Verso Blueprint · commit-pinned GitHub source