Textbook / teaching anchor
Basics of quantum information
“quantum state vectors are unit vectors with respect to the Euclidean norm.”
Beginner-friendly state-vector, measurement, multi-system, and circuit explanations.
Reading mode
Start visually; reveal formalism only when you want it.
Beginner layer · before the formal matrix API
A qubit is a two-entry complex vector
Do not start by thinking about a mysterious physical particle. For the algorithms in this library, start with two labels, |0⟩ and |1⟩, and attach a complex amplitude to each.
q₀
|ψ⟩
state
α|0⟩+β|1⟩
- Basis|0⟩ and |1⟩ are the two computational labels.
- Amplitudeα and β are not probabilities; their squared magnitudes are.
- NormalizationThe two measurement probabilities must add to one.
- MatrixA quantum gate acts on the amplitude vector by matrix multiplication.
Textbook / teaching anchor
Quantum Computation and Quantum Information
Standard textbook reference for quantum mechanics, qubits, gates, and the circuit model.
Strict mathematics, after the picture
The equations behind the intuition
\[|\psi\rangle=\alpha|0\rangle+\beta|1\rangle\]
\[|\alpha|^2+|\beta|^2=1\]
\[P(0)=|\alpha|^2,\qquad P(1)=|\beta|^2\]
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
“quantum state vectors are unit vectors with respect to the Euclidean norm.”
Beginner-friendly state-vector, measurement, multi-system, and circuit explanations.
Textbook / teaching anchor
Quantum Computation and Quantum Information
Standard textbook reference for quantum mechanics, qubits, gates, and the circuit model.
Learn Lean while learning quantum computing
Lean idea: finite indices
abbrev Matrix (rows cols : Nat) (α : Type u) := Fin rows → Fin cols → α`Fin 2` means exactly two legal indices. Lean makes an out-of-range basis label impossible to type.
The full proof-backed declarations for this chapter are shown immediately below.
Shared foundations · Chapter 1 of 9
Vectors, matrices, and basis states
Fix the finite matrix model, pointwise equality, dimensions, and resource records used by every later certificate.
Lean modules used in this chapter
QuantumBlockEncoding/Core.leanQuantumBlockEncoding/Resources.lean
Textbook lesson
Build the idea before opening the proof
A quantum state is a complex column vector. For n qubits its dimension is 2^n, so every basis label is a finite index from 0 to 2^n-1.
States are normalized vectors
\[|\psi\rangle=\sum_{j=0}^{2^n-1}\psi_j|j\rangle,\qquad \sum_j|\psi_j|^2=1.\]
The amplitudes are complex numbers and the squared magnitudes sum to one. An unnormalized data vector must be rescaled before it can be the exact output of a unitary.
Matrices act on columns
\[(U|\psi\rangle)_i=\sum_j U_{ij}\psi_j.\]
ASPBE fixes column-vector, left-action semantics. This convention determines gate order, first-column state preparation, and clean-block indices.
Equality becomes finite obligations
\[A=B\iff \forall i,j,\ A_{ij}=B_{ij}.\]
Lean does not accept a diagram as evidence. It checks each finite index, or a reusable theorem that implies all of those entry equalities.
Check your understanding
Before continuing, be able to explain why a one-qubit gate is a 2 by 2 matrix and a two-qubit gate is a 4 by 4 matrix.
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
Pointwise matrix equality
QuantumBlockEncoding.Matrix.PointwiseEq
DeclarationCompiled
Full routeCompiled
\[A = B \;\Longleftrightarrow\; \forall i\,j,\; A_{ij}=B_{ij}.\]
What it says
Two finite matrices are equal when every indexed entry agrees.
Why it matters
Matrix goals become explicit finite entry goals that Lean can rewrite. Block extraction and candidate validation are ultimately entrywise claims.
How the proof goes
Expose row and column indices, prove the scalar equality, then recover matrix equality.
- Uses
QuantumBlockEncoding.Matrix- Still outside this result
- None for this local declaration.
Route closure
Natural-language steps and Lean objects
| Mathematical step | Lean object or step |
|---|---|
| Choose arbitrary indices. | intro i j |
| Reduce the matrix claim to the selected entry. | apply Matrix.ext |
Open the Lean statement and source links
def PointwiseEq {rows cols : Nat} {α : Type u}
(a b : Matrix rows cols α) : Prop :=
∀ i j, a i j = b i j
/-- The zero finite matrix. -/Local declaration · Verso Blueprint · commit-pinned GitHub source
Lean result
Executable resource records
QuantumBlockEncoding.Resource
DeclarationCompiled
Full routeCompiled
\[r=(q_{\mathrm{anc}},q_{\mathrm{tot}},d,n_{1q},n_{2q}).\]
What it says
A candidate carries named resource counts instead of an informal cost label.
Why it matters
The proof object and the engineering cost can be compared without conflating them. Candidate search needs deterministic, auditable scoring fields.
How the proof goes
Represent each resource coordinate as data and derive decidable comparison support.
- Uses
QuantumBlockEncoding.gridSize- Still outside this result
- None within the declared reusable route.
Route closure
QuantumBlockEncoding.ExecutableResourceCertificate.resource_eq_program_resourceQuantumBlockEncoding.ExecutableResourceCertificate.cost_gateCountQuantumBlockEncoding.ExecutableResourceCertificate.cost_depth
Natural-language steps and Lean objects
| Mathematical step | Lean object or step |
|---|---|
| Store each cost coordinate. | structure Resource |
| Expose values to scoring and export code. | deriving Repr |
Open the Lean statement and source links
structure Resource where
oneQubit : Nat := 0
cnot : Nat := 0
oracleCalls : Nat := 0
pureAncilla : Nat := 0
depth : Nat := 0
deriving Repr, DecidableEqLocal declaration · Verso Blueprint · commit-pinned GitHub source