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

Beginner layer · how block encodings are constructed

PREPARE, SELECT, and UNPREPARE turn structured sums into circuits

Most useful matrices have structure. Instead of synthesizing one enormous unitary from scratch, expose that structure: sparse locations, sparse values, permutations, or a linear combination of simpler unitaries.

The standard LCU skeleton used repeatedly by block-encoding constructions.

selector |0⟩ PREPARESELECTPREPARE† |0⟩

system |ψ⟩ U_j A|ψ⟩/α

PREPARECreate a superposition over terms or sparse slots.
SELECTApply the operation indexed by that slot.
AmplitudeLoad the coefficient associated with the chosen term.
UNPREPAREInterfere the selector branches so the clean block becomes the desired weighted sum.

Textbook / teaching anchor

Lecture Notes on Quantum Algorithms for Scientific Computation

Lin Lin

Scientific-computing route from quantum preliminaries to block encoding, QSP, and QSVT.

Textbook / teaching anchor

Quantum singular value transformation and beyond

András Gilyén, Yuan Su, Guang Hao Low, Nathan Wiebe

Research anchor for block encoding and singular-value transformation.

Strict mathematics, after the picture

The equations behind the intuition

\[A=\sum_{j=0}^{L-1} a_jU_j\]

\[\operatorname{PREPARE}|0\rangle=\sum_j\sqrt{p_j}|j\rangle\]

\[\operatorname{SELECT}=\sum_j|j\rangle\!\langle j|\otimes U_j\]

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

Textbook / teaching anchor

Lecture Notes on Quantum Algorithms for Scientific Computation

Lin Lin

Scientific-computing route from quantum preliminaries to block encoding, QSP, and QSVT.

Textbook / teaching anchor

Quantum singular value transformation and beyond

András Gilyén, Yuan Su, Guang Hao Low, Nathan Wiebe

Research anchor for block encoding and singular-value transformation.

Learn Lean while learning quantum computing

Lean idea: composition becomes reusable lemmas

productExactCleanBlockCertificate
partialPermutationCertificate
QSVTConsumerContract

Instead of proving each paper from zero, ASPBE keeps small proof-producing constructors for recurring routes.

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

Block encoding · Chapter 6 of 9

Construction routes and composition rules

Reuse permutation, one-sparse, LCU, product, dilation, and QSVT interfaces instead of rediscovering each route per benchmark.

Lean modules used in this chapter

QuantumBlockEncoding/BlockEncodingClassics.lean
QuantumBlockEncoding/BandedSparseAccess.lean
QuantumBlockEncoding/BandedSparseAccessPrimitive.lean

Textbook lesson

Build the idea before opening the proof

Most useful proofs follow a small number of constructions. Route selection should happen before expanding a large circuit product.

Sparse routing

\[O_c|j\rangle=|c(j)\rangle.\]

When support is a reversible finite map, the proof reduces to routed basis indices and vanishing off-support entries.

Banded sparse access

\[U_A^{(l)}:|0^{n-l}\rangle|s\rangle\mapsto|r_{s0}\rangle,\qquad U^{SUM}:|r\rangle|i\rangle\mapsto|r+i\bmod2^n\rangle|i\rangle.\]

ASPBE proves the arbitrary-size semantic composition and its unitary permutation matrix. The source paper's general resource formula remains a separate compiler theorem.

Composition

\[\operatorname{block}(U_BU_A)=BA.\]

Compatible clean-block certificates compose. Register compatibility and normalizers still have to match.

Consumer boundary

\[U_A\leadsto p^{(\mathrm{SV})}(A/\alpha).\]

QSVT does not repair an invalid source encoding. The source certificate and the polynomial approximation are separate proof obligations.

Check your understanding

Choose one route for a diagonal matrix and state which oracle or finite map must still be implemented.

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 TB
  Core["Core / Resources"] --> State["StatePreparation"]
  Core --> Circuit["Circuit"]
  Circuit --> Sem["CircuitSemantics"]
  Core --> Block["BlockEncoding"]
  State --> Classics["BlockEncodingClassics"]
  Sem --> Classics
  Block --> Classics
  Classics --> Case1["ColdStartTransferE1<br/>BE Case 1"]
  Classics --> Case2["CubicStatePreparation<br/>BE Case 2"]
  Classics --> Paper["GHL2025 / RobinHeat"]
  State --> Case2
  Auto["Automation / Literature<br/>OpenProblems"] --> Case1
  Auto --> Case2

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

Banded sparse address access

QuantumBlockEncoding.BandedSparseAccess.accessEquiv_clean_slot

DeclarationCompiled Full routeCompiled

|0^{n-l}\rangle|s\rangle|i\rangle\mapsto|r_{s0}+i\bmod 2^n\rangle|i\rangle.

What it says

The arbitrary-size loader-plus-SUM semantics is unitary, and a clean three-bit instance is refined to the exact primitive basis.

Why it matters

The source-dependent loader chooses the first-row offset; the reusable SUM operation shifts it to row i. The generic semantics matches the cited construction, while the finite primitive witness proves that the compiler boundary is executable and oracle-free.

How the proof goes

Compose the generic finite equivalences, then instantiate an XOR-three loader, compile its modular adder to X/RY/RZ/CX, and prove clean action, unitarity, and zero unresolved oracle calls.

Uses: QuantumBlockEncoding.BandedSparseAccess.modularSumEquiv; QuantumBlockEncoding.BandedSparseAccess.accessMatrix_unitary; QuantumBlockEncoding.BandedSparseAccess.primitiveAccess3Program_eval
Still outside this result: None within the declared semantic-plus-finite-compiler route. The paper's arbitrary-size one-qubit/CNOT upper bound remains a separate general compiler theorem.

Route closure

Natural-language steps and Lean objects

Mathematical step	Lean object or step
Load the first-row band offset.	`liftLoaderEquiv / primitiveOffset3`
Add the preserved row modulo 2^n.	`modularSumEquiv / modularAdd3ReversibleProgram`
Prove the clean selected address.	`accessEquiv_clean_slot / primitiveAccess3_cleanAction`
Refine the finite witness to primitive matrices.	`primitiveAccess3Program_eval`

Open the Lean statement and source links

theorem accessEquiv_clean_slot
    (n : Nat) {l : Nat}
    (offset : Fin (2 ^ l) → Word n)
    (loader : Equiv.Perm (Word n))
    (loader_spec : ∀ slot, loader (slotWord n slot) = offset slot)
    (slot : Fin (2 ^ l)) (row : Word n) :
    accessEquiv n loader (slotWord n slot, row) =
      (offset slot + row, row) := by

Local declaration · Verso Blueprint · commit-pinned GitHub source

Lean result

Partial-permutation certificate

QuantumBlockEncoding.BlockEncodingClassics.partialPermutationCertificate

DeclarationCompiled Full routeCompiled

A_{ij}\in\{0,1\},\quad \text{at most one supported entry per routed index}.

What it says

A finite partial permutation satisfying the declared support conditions yields an exact clean block.

Why it matters

The circuit route becomes finite index routing rather than dense matrix algebra. BE Case 1 can reuse this route and avoid an unconstrained circuit search.

How the proof goes

Construct the routed unitary and prove the clean ancilla block entry by entry.

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

Route closure

QuantumBlockEncoding.BlockEncodingClassics.partialPermutationCertificate

Natural-language steps and Lean objects

Mathematical step	Lean object or step
Establish the finite routing conditions.	`partialPermutationCertificate`
Read the clean block theorem.	`ExactCleanBlock.clean_eq_target`

Open the Lean statement and source links

def partialPermutationCertificate {system total : Nat}
    (embed : Fin system -> Fin total) (p : Fin total -> Fin total)
    (A : Matrix system system Rat)
    (h :
      forall row col : Fin system,
        (if embed row = p (embed col) then 1 else 0) = A row col) :
    ExactCleanBlock system total where
  U := permMatrix p
  A := A
  embed := embed
  blockProof := cleanBlockBy_permMatrix_eq_target_of_entry embed p A h

Local declaration · Verso Blueprint · commit-pinned GitHub source

Lean result

Product closure for exact clean blocks

QuantumBlockEncoding.BlockEncodingClassics.productExactCleanBlockCertificate

DeclarationCompiled Full routeCompiled

\operatorname{block}(U_B U_A)=BA.

What it says

Compatible exact clean-block certificates compose into a certificate for the matrix product.

Why it matters

Certified components can be recombined as a proof-producing population operation. It is the formal counterpart of crossing over reusable constructions.

How the proof goes

Expand the projected product, use both component block identities, and reassociate finite sums.

Uses: QuantumBlockEncoding.BlockEncodingClassics.ExactCleanBlock; QuantumBlockEncoding.BlockEncodingClassics.matrix_mul_congr_pointwise
Still outside this result: None for this local declaration.

Route closure

QuantumBlockEncoding.BlockEncodingClassics.productExactCleanBlockCertificate

Natural-language steps and Lean objects

Mathematical step	Lean object or step
Substitute component clean blocks.	`ExactCleanBlock.clean_eq_target`
Identify the matrix product.	`matrix_mul_congr_pointwise`

Open the Lean statement and source links

def productExactCleanBlockCertificate {system totalLeft totalRight : Nat}
    (left : ExactCleanBlock system totalLeft)
    (right : ExactCleanBlock system totalRight) : LCUCertificate system :=
  productCleanBlockCertificate
    (ExactCleanBlock.toLCUCertificate left)
    (ExactCleanBlock.toLCUCertificate right)

/-- Tensor-style resource score: parallel depth is the maximum of two depths. -/

Local declaration · Verso Blueprint · commit-pinned GitHub source

Lean result

QSVT consumer boundary

QuantumBlockEncoding.BlockEncodingClassics.QSVTConsumerContract

DeclarationCompiled Full routeCompiled

U_A\leadsto p^{(\mathrm{SV})}(A/\alpha).

What it says

The library records what a later QSVT stage may assume from a supplied block encoding.

Why it matters

QSVT is kept as an explicit consumer contract rather than treated as a proved end-to-end implementation. The hinted hard route can stop rediscovering the interface between a diagonal oracle and QSVT.

How the proof goes

Package the exact preconditions and expected transformed-operator relation as a typed boundary.

Uses: QuantumBlockEncoding.BlockEncodingClassics.HermitianDilationContract
Still outside this result: None within the declared reusable route.

Route closure

Natural-language steps and Lean objects

Mathematical step	Lean object or step
Provide a source block encoding.	`QSVTConsumerContract.source`
State the consumer obligation.	`QSVTConsumerContract`

Open the Lean statement and source links

structure QSVTConsumerContract (system total : Nat) where
  input : ExactCleanBlock system total
  polynomialDescription : String
  sideConditions : Prop
  outputStatement : Prop
  sideConditionProof : sideConditions
  outputProof : outputStatement

/-- Zero-error approximate incumbent at the clean-block level. -/

Local declaration · Verso Blueprint · commit-pinned GitHub source