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

Beginner layer · why the first column matters

Applying U to |0…0⟩ simply selects the first column of U

This is the bridge between circuit language and matrix language. Physicists write U|0⟩; Lean can check the same statement one output amplitude at a time.

State-action and first-column views are the same certificate.

q |0…0⟩ U column₀(U)=|ψ⟩

InputThe vector |0…0⟩ has a single 1 in the zero position.
MultiplyEvery matrix column except column zero is multiplied by 0.
ResultThe output is exactly column zero.
ReuseThat theorem becomes a compact interface for later LCU and oracle constructions.

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=\operatorname{column}_0(U)\]

\[U_{i,0}=\psi_i\]

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: `iff` proves two descriptions are equivalent

firstColumnMatches_iff_applyVec_zeroKet

The theorem is deliberately bidirectional: a column proof can become a state-action proof and vice versa.

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

State preparation · Chapter 4 of 9

Reading and reusing a preparation certificate

Connect the ket equation to a matrix column, package the proof, and reuse exact preparation where an approximate interface is expected.

Lean modules used in this chapter

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

Textbook lesson

Build the idea before opening the proof

A certificate is useful because later code can consume one trusted object instead of repeating the matrix calculation.

Why column zero appears

\[U|0^n\rangle=\operatorname{column}_0(U).\]

The zero ket has one nonzero amplitude at index zero. Matrix-vector multiplication therefore discards every column except the first.

What the record stores

\[\text{normalized target}+\text{unitary U}+\text{first-column proof}.\]

Each field has a different failure mode. Keeping them separate prevents a correct first column from hiding a nonunitary completion.

Exact before approximate

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

An exact certificate can enter an approximate search unchanged. Positive error needs a declared metric and a new bound.

Check your understanding

Explain why matching column zero alone does not prove that a candidate is physically implementable.

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

The ket equation is a first-column statement

QuantumBlockEncoding.ConcreteSemantics.firstColumnMatches_iff_applyVec_zeroKet

DeclarationCompiled Full routeCompiled

\operatorname{column}_0(U)=\psi\iff U\lvert0^n\rangle=\lvert\psi\rangle.

What it says

Matrix action on the all-zero ket selects exactly the first column of the unitary.

Why it matters

There are two common ways to say the same fact: physicists write a ket equation, while the finite Lean model compares indexed amplitudes. This bridge keeps proofs and circuit explanations in the same convention.

How the proof goes

Acting on a basis vector selects one matrix column; function extensionality then turns vector equality into entrywise equality.

Uses: QuantumBlockEncoding.FirstColumnMatches; QuantumBlockEncoding.ConcreteSemantics.applyVec_zeroKet
Still outside this result: None within the declared reusable route.

Route closure

Natural-language steps and Lean objects

Mathematical step	Lean object or step
Apply the matrix to the zero basis ket.	`applyVec_zeroKet`
Compare every output amplitude.	`funext / congrFun`

Open the Lean statement and source links

theorem firstColumnMatches_iff_applyVec_zeroKet
    {α : Type u} [NonAssocSemiring α] {qubits : Nat}
    (operator : Matrix (gridSize qubits) (gridSize qubits) α)
    (target : StatePreparationTarget α qubits) :
    FirstColumnMatches operator target ↔
      applyVec operator (zeroKet qubits) = target.amplitudes := by

Local declaration · Verso Blueprint · commit-pinned GitHub source

Lean result

A verified preparer exposes its amplitudes

QuantumBlockEncoding.VerifiedStatePreparation.firstColumn

DeclarationCompiled Full routeCompiled

U_{i,0}=\psi_i.

What it says

Once the certificate is built, downstream proofs can read its first-column identity directly.

Why it matters

The certificate hides the packaging work but does not weaken the statement. Prepared amplitudes are often the input to later LCU or oracle constructions.

How the proof goes

Project the stored preparation proof from the verified record.

Uses: QuantumBlockEncoding.VerifiedStatePreparation
Still outside this result: None for this local declaration.

Route closure

QuantumBlockEncoding.VerifiedStatePreparation.firstColumn

Natural-language steps and Lean objects

Mathematical step	Lean object or step
Read the certified state-action field.	`verified.preparationProof`
Expose it through the public theorem.	`verified.firstColumn`

Open the Lean statement and source links

theorem firstColumn
    (verified : VerifiedStatePreparation α qubits) :
    verified.candidate.preparesTarget :=
  verified.preparationProof

Local declaration · Verso Blueprint · commit-pinned GitHub source

Lean result

Exact preparation can enter an approximate interface

QuantumBlockEncoding.VerifiedStatePreparation.asZeroErrorApprox

DeclarationCompiled Full routeCompiled

\varepsilon=0.

What it says

An exact certificate is also an approximate certificate with error zero.

Why it matters

The tolerance ladder can reuse exact work instead of changing certificate formats. Exact and approximate searches need one stable consumer boundary.

How the proof goes

Reuse normalization, unitarity, and preparation proofs while setting the approximation field to the exact predicate.

Uses: QuantumBlockEncoding.VerifiedStatePreparation
Still outside this result: None for this local declaration.

Route closure

QuantumBlockEncoding.VerifiedStatePreparation.asZeroErrorApprox

Natural-language steps and Lean objects

Mathematical step	Lean object or step
Keep the same candidate and proofs.	`verified.candidate / normalizationProof / unitaryProof`
Set the error to zero.	`epsilon := 0`

Open the Lean statement and source links

def asZeroErrorApprox [OfNat α 0]
    (verified : VerifiedStatePreparation α qubits) :
    VerifiedApproximateStatePreparation α qubits where
  approxCandidate := {
    candidate := verified.candidate
    epsilon := 0
    approximationBound := verified.candidate.preparesTarget
  }
  normalizationProof := verified.normalizationProof
  unitaryProof := verified.unitaryProof
  approximationProof := verified.preparationProof

Local declaration · Verso Blueprint · commit-pinned GitHub source