QuantumComputinglib learn · inspect · formalize
Checked on this commit 2,822 public declarations commit 07559c3d051f Build record
Reading mode Start visually; reveal formalism only when you want it.

Beginner layer · second ASPBE problem

A general matrix is not a quantum gate — block encoding hides it inside one

Quantum gates must be unitary, but the matrix A you want to use may be non-unitary. The trick is to build a larger unitary U whose clean ancilla corner equals A up to a known scale.

The ancilla is prepared and projected in |0⟩; the system sees the clean block A/α.
anc |0⟩ U_Aproject 0 |0⟩
sys |ψ⟩ U_A A|ψ⟩/α
  1. ProblemA may shrink, amplify, or otherwise fail the unitary condition.
  2. Add roomIntroduce ancilla qubits so a larger matrix can remain unitary.
  3. Hide AArrange for the ancilla-zero block to be A/α.
  4. Use itLater algorithms can manipulate the encoded matrix while only implementing the unitary U_A.

Strict mathematics, after the picture

The equations behind the intuition

\[U_A=\begin{pmatrix}A/\alpha&*\\ *&*\end{pmatrix}\]
\[\left\|A-\alpha(\langle0^a|\otimes I)U_A(|0^a\rangle\otimes I)\right\|\le\varepsilon\]

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

Learn Lean while learning quantum computing

Lean idea: projection equality is the acceptance test

candidate.blockContainsTarget : ∀ i j, U (clean i) (clean j) = A i j / α

The library does not accept a circuit because a simulator looks close. The selected matrix entries are an explicit proposition.

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

Block encoding · Chapter 5 of 9

The block-encoding contract

State the block contract with normalization, explicit register layout, and a verifier-facing certificate record.

Lean modules used in this chapter
  • QuantumBlockEncoding/BlockEncoding.lean

Textbook lesson

Build the idea before opening the proof

Block encoding is an input model for a generally nonunitary matrix: a larger unitary exposes the desired operator when clean ancillas are projected onto zero.

Exact clean block

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

The upper-left wording is safe only after register order is fixed. ASPBE therefore records the clean index and layout as part of the contract.

Proof style A: project the matrix

\[\langle0^a,i|U|0^a,j\rangle=(A/\alpha)_{ij}.\]

This is the direct form of Definition 1, Eq. (2), in arXiv:2205.00081. It is usually the shortest Lean proof for a finite circuit: fix i and j, unfold the clean register indices, and prove one matrix entry.

Proof style B: follow an arbitrary input

\[U|0^a\rangle|\psi\rangle=|0^a\rangle\widetilde A|\psi\rangle+\sqrt{1-\|\widetilde A|\psi\rangle\|^2}\,|\sigma_\perp\rangle.\]

Equations (3)-(5) of arXiv:2205.00081 express the same clean block through state evolution: the failure state has zero clean projection and unit norm. ASPBE proves the basis-action/projected-entry equivalence; linearity gives arbitrary inputs. A claimed normalized failure branch still needs its own unitarity and norm proof.

Approximate form

\[\|A-\alpha(\langle0^a|\otimes I)U(|0^a\rangle\otimes I)\|\le\varepsilon.\]

The norm and tolerance must be named. Approximation is a controlled relaxation, not permission to change the target matrix.

Normalization affects success

\[p(0^a)=\|A|b\rangle\|^2/\alpha^2.\]

A larger alpha can make unitary completion easier but lowers clean-ancilla success probability. Resource comparisons must report it.

Check your understanding

For a proposed U, write the exact row and column indices selected when every ancilla is zero.

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

Block encoding: The block-encoding contract editable Mermaid source 
flowchart LR
  T["Target operator A<br/>and scale α"] --> R["Fix ancillas, norm,<br/>and register order"]
  R --> C["Choose a construction<br/>family and unitary U"]
  C --> U["Prove U is unitary"]
  C --> B["Prove the clean block<br/>‖A − α Π U Π†‖ ≤ ε"]
  U --> L["Lean block-encoding<br/>certificate"]
  B --> L
  L --> E["Export and check one<br/>certified finite instance"]

  classDef target fill:#ffffff,stroke:#49677d,color:#1f2e39,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,R target;
  class C,U,B 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

Candidate cost is derived from its layout

QuantumBlockEncoding.OperatorBlockEncodingCandidate.cost
DeclarationCompiled Full routeCompiled
\[c(U)=(a,q,d,n_{1q},n_{2q},\ldots).\]

What it says

The block-encoding candidate exposes a deterministic cost tuple from its declared registers and circuit resources.

Why it matters

A candidate is not accepted only because its matrix works; alternatives remain rankable. The search layer needs a stable objective before proof attempts consume more budget.

How the proof goes

Read the layout and circuit fields and assemble the canonical cost record.

Uses
QuantumBlockEncoding.OperatorBlockEncodingCandidate; QuantumBlockEncoding.RegisterLayout; QuantumBlockEncoding.BlockEncodingCost
Still outside this result
None within the declared reusable route.

Route closure

Natural-language steps and Lean objects

Mathematical stepLean object or step
Read ancillary and signal sizes.candidate.layout
Build the score tuple.candidate.cost
Open the Lean statement and source links 
def cost (candidate : OperatorBlockEncodingCandidate α systemQubits) :
    BlockEncodingCost :=
  {
    auxiliaryQubits := candidate.auxiliaryQubits
    gateCount := candidate.resource.gates
    depth := candidate.resource.depth
    oracleCalls := candidate.resource.oracleCalls
  }

Local declaration · Verso Blueprint · commit-pinned GitHub source

Lean result

Exact certificates are zero-error approximate certificates

QuantumBlockEncoding.VerifiedOperatorBlockEncoding.asZeroErrorApprox
DeclarationCompiled Full routeCompiled
\[\left\|A-\alpha\Pi U\Pi^\dagger\right\|=0.\]

What it says

Every exact verified block encoding can be reused where an approximation with epsilon zero is expected.

Why it matters

Exactness is the strongest point on the tolerance ladder. The harness can begin exact and relax epsilon without changing the consumer interface.

How the proof goes

Rewrite with the exact block identity; the residual is the zero matrix.

Uses
QuantumBlockEncoding.VerifiedOperatorBlockEncoding; QuantumBlockEncoding.QueryOperatorTarget
Still outside this result
None for this local declaration.

Route closure

Natural-language steps and Lean objects

Mathematical stepLean object or step
Use the stored exact equality.verified.correct
Package error zero.verified.asZeroErrorApprox
Open the Lean statement and source links 
def asZeroErrorApprox [OfNat α 0]
    (v : VerifiedOperatorBlockEncoding α systemQubits) :
    VerifiedApproximateOperatorBlockEncoding α systemQubits where
  approxCandidate := {
    candidate := v.candidate
    epsilon := 0
    approximationBound := v.candidate.blockContainsTarget
  }
  unitaryProof := v.unitaryProof
  approximationProof := v.blockProof

Local declaration · Verso Blueprint · commit-pinned GitHub source