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

Suggested backgroundBasics of quantum informationIBM Quantum Learning / John Watrous
“quantum state vectors are unit vectors with respect to the Euclidean norm.”
Quantum circuitsIBM Quantum Learning / John Watrous
“The flow of information along the wires goes from left to right”
Lecture Notes on Quantum Algorithms for Scientific ComputationLin Lin
“A more general input model, as will be discussed in this chapter, is called ‘block encoding’.”
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.

Part II · encompassing block-encoding layer

Block encoding

Given an operator \(A\), place the scaled operator inside a larger unitary. The contract says exactly which ancilla block is selected and how normalization and approximation are interpreted.

\[\left\|A-\alpha\Pi U\Pi^\dagger\right\|\le\varepsilon\]

Read the notation before the circuit

Four choices determine the contract

Ancillas
Extra qubits make room for the larger unitary and are projected onto a declared clean state.
Register order
The index convention identifies which matrix rows and columns form the signal block.
Normalization \(\alpha\)
The selected block represents \(A/\alpha\), so the scale is part of correctness.
Error \(\varepsilon\)
Exact encoding has zero error; approximate routes must name both a norm and a tolerance.

Encompassing construction certificate

What ASPBE has to establish

A candidate is not accepted because one small matrix looks right. The layout, unitarity, projected block, scale, and declared resource record are checked as separate obligations.

Block-encoding proof and export flow 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;

Source-audited additions · not yet compiled roots

Diagonal operators and structured Fourier suppliers

be-diagonal

Unitary and non-unitary diagonal operators

Separate phase operators from dilated filters and prove matched space–time–accuracy contracts, including cleanup and error-scale adapters.

Planned
Inspect pinned upstream memory (1 routes)

OpenAI Math snapshot adc7f1241b42 · upstream Lean 4.34.1 · local migration target 4.33.0. Source placement does not certify an adapter, the whole chapter, or an SP/BE construction.

  • oai-unitary-synthesis-boolean-oracle

    preprints/Polynomial-Time-Unitary-Synthesis-from-a-Boolean-Oracle-October-5-2026

    oracle-assisted unitary synthesis frontier directly relevant to ASPBE synthesis semantics

    Upstream evidence: manuscript-only-in-current-audit. benchmark-only. Not local admission.

    Next boundary: compare target/operator/oracle/resource contract with the ASPBE synthesis API before formal route creation

be-fourier-suppliers

Fourier and structured linear-operator suppliers

Connect exact Fourier circuit resources and structured operator descriptions to the shared circuit and block interfaces without treating either as an automatic block encoding.

Planned
Inspect pinned upstream memory (1 routes)

OpenAI Math snapshot adc7f1241b42 · upstream Lean 4.34.1 · local migration target 4.33.0. Source placement does not certify an adapter, the whole chapter, or an SP/BE construction.

  • oai-exact-fourier

    Computability/FourierCircuit

    exact Fourier-circuit construction and resource theorem; supplier to Fourier/QPE chapters after circuit-model adaptation

    Upstream evidence: comparator-backed. source-route. Not local admission.

    Next boundary: compare circuit ordering, gate set and cost tuple with the local circuit/resource API; do not present the Fourier result as a block encoding or QPE certificate

The main inclusion-like connection

State Preparation supplies a nested PREPARE subproblem

A certified state-preparation circuit can supply a PREPARE oracle for an LCU, Gram, or purification-based construction. Its first-column theorem becomes a dependency; it does not by itself prove the clean-block identity.

Read the block contract Compare construction routes See certified cases →