Textbook / teaching anchor
Quantum circuits
Visual circuit-model reference.
Reading mode
Start visually; reveal formalism only when you want it.
Beginner layer · the circuit model
A quantum circuit is a time-ordered product of unitary gates
A wire tells you where the state lives; a box tells you which operation happens next. Read time from left to right, but remember that matrix products act on state vectors from the right.
q₀
|0⟩
HSHT
|ψout⟩
- DrawPlace one operation after another on the wire.
- ReadThe leftmost gate happens first.
- MultiplyThe total unitary is G_m⋯G_1.
- VerifyLean fixes this order once so diagrams and matrix proofs cannot silently disagree.
Textbook / teaching anchor
Quantum Computation and Quantum Information
“Computers are physical objects, and computations are physical processes.”
Standard textbook reference for quantum mechanics, qubits, gates, and the circuit model.
Strict mathematics, after the picture
The equations behind the intuition
\[|\psi_{\mathrm{out}}\rangle=G_m\cdots G_2G_1|\psi_{\mathrm{in}}\rangle\]
\[U^\dagger U=UU^\dagger=I\]
Every symbol used here is connected below to a compiled declaration or a clearly marked research-source formula.
Textbook / teaching anchor
Quantum circuits
Visual circuit-model reference.
Textbook / teaching anchor
Quantum Computation and Quantum Information
“Computers are physical objects, and computations are physical processes.”
Standard textbook reference for quantum mechanics, qubits, gates, and the circuit model.
Learn Lean while learning quantum computing
Lean idea: definitions compute
evalGateMatrices [G₁, G₂, …, Gₘ] = Gₘ ⬝ … ⬝ G₂ ⬝ G₁The evaluator is a definition, and later theorems prove that circuit syntax and matrix meaning use the same order.
The full proof-backed declarations for this chapter are shown immediately below.
Shared foundations · Chapter 2 of 9
Gates, unitaries, and circuit meaning
Separate gate syntax from matrix evaluation and make register order an explicit part of the semantic boundary.
Lean modules used in this chapter
QuantumBlockEncoding/Circuit.leanQuantumBlockEncoding/CircuitSemantics.leanQuantumBlockEncoding/ConcreteSemantics.lean
Textbook lesson
Build the idea before opening the proof
A circuit is an ordered program; its denotation is one unitary matrix. The list order and multiplication order must be stated once and then reused everywhere.
Unitary evolution
\[U^\dagger U=I,\qquad |\psi'\rangle=U|\psi\rangle.\]
A gate preserves norm. ASPBE's concrete certificates use Mathlib's unitary group, while symbolic paper models keep unproved oracle unitarity as an explicit contract.
Composition order
\[[g_1,g_2,\ldots,g_m]\mapsto G_m\cdots G_2G_1.\]
The rightmost matrix acts first. Reversing this convention can preserve dimensions while changing the algorithm, so the evaluator is a named library definition.
Registers are part of meaning
\[|a\rangle|i\rangle\leftrightarrow a\,2^n+i.\]
Flattening ancilla and system registers requires one fixed order. Projection lemmas prove that the flat index and product-register views select the same entries.
Check your understanding
Given gates G then V, write the final state and the combined matrix without reversing their order.
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
C["Fixed mathematical<br/>contract"] --> O["Named proof<br/>obligations"]
O --> P["Candidate routes<br/>with provenance"]
P --> L{"Lean gate"}
L -- "proof fails" --> F["Classified failure<br/>and next local lemma"]
F --> P
L -- "certificate compiles" --> X["Finite export<br/>and circuit check"]
X --> D["Documented result<br/>with stated scope"]
classDef contract fill:#f8f5ee,stroke:#826a32,color:#222222,stroke-width:1.5px;
classDef process fill:#ffffff,stroke:#64747a,color:#222222,stroke-width:1.25px;
classDef gate fill:#edf5f1,stroke:#2f7355,color:#18382b,stroke-width:1.5px;
classDef feedback fill:#fff2ef,stroke:#a44b3f,color:#4a2520,stroke-width:1.25px;
class C contract;
class O,P,X,D process;
class L gate;
class F feedback;
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
Circuit matrix evaluation
QuantumBlockEncoding.evalGateMatrices
DeclarationCompiled
Full routeCompiled
\[\mathrm{Eval}([g_1,\ldots,g_m])=G_m\cdots G_1.\]
What it says
A list of gate matrices is folded into one matrix in the library's declared application order.
Why it matters
The list is executable syntax; its fold is the matrix used by proofs. Without one order convention, circuit diagrams and matrix products can silently disagree.
How the proof goes
Recursively multiply the next gate matrix on the side fixed by the semantics.
- Uses
QuantumBlockEncoding.GateMatrix;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 |
|---|---|
| Empty circuit is identity. | evalGateMatrices [] |
| Compose the next gate. | evalGateMatrices (g :: gs) |
Open the Lean statement and source links
def evalGateMatrices {α : Type u} [OfNat α 0] [OfNat α 1]
[HAdd α α α] [HMul α α α] {qubits : Nat}
(gates : List (GateMatrix α qubits)) :
Matrix (qubitDim qubits) (qubitDim qubits) α :=
gates.foldl (fun acc gateMatrix => Matrix.mul gateMatrix.matrix acc)
(Matrix.identity (qubitDim qubits) α)Local declaration · Verso Blueprint · commit-pinned GitHub source
Lean result
Flat and product-register clean blocks agree
QuantumBlockEncoding.ConcreteSemantics.signalSystemBlockProjection_eq_cleanBlockProduct
DeclarationCompiled
Full routeCompiled
\[\Pi_s U\Pi_s^\dagger=\operatorname{cleanBlockProduct}(s,U).\]
What it says
The two ASPBE block-projection views are pointwise equal under the shared register order.
Why it matters
A circuit-semantics proof can be consumed by classic block-encoding arithmetic without index reconstruction. Register-shape mismatches were a repeated historical failure class.
How the proof goes
Both definitions use the same signal-major flattened index, so the pointwise proof is definitional.
- Uses
QuantumBlockEncoding.signalSystemBlockProjection;QuantumBlockEncoding.BlockEncodingClassics.cleanBlockProduct- Still outside this result
- None within the declared reusable route.
Route closure
QuantumBlockEncoding.ConcreteSemantics.exactCleanBlockOfSignalProjectionQuantumBlockEncoding.ConcreteSemantics.exactCleanBlockOfSignalProjection_correct
Natural-language steps and Lean objects
| Mathematical step | Lean object or step |
|---|---|
| Fix system row and column. | intro row col |
| Unfold the shared index. | rfl |
Open the Lean statement and source links
theorem signalSystemBlockProjection_eq_cleanBlockProduct
{signalDim systemDim : Nat}
(operator : Matrix (signalDim * systemDim) (signalDim * systemDim) Rat)
(signalIndex : Fin signalDim) :
Matrix.PointwiseEq
(signalSystemBlockProjection
signalDim systemDim systemDim operator signalIndex)
(BlockEncodingClassics.cleanBlockProduct signalIndex operator) := byLocal declaration · Verso Blueprint · commit-pinned GitHub source
Lean result
Circuit-to-block extraction target
QuantumBlockEncoding.CircuitMatrixSemantics.blockExtractionTarget
DeclarationCompiled
Full routeCompiled
\[(\langle0^a\rvert\otimes I)\,U\,(|0^a\rangle\otimes I)=A/\alpha.\]
What it says
Circuit semantics selects the signal-system block that must match the scaled target operator.
Why it matters
Ancillas are fixed to zero on both sides; the remaining indices are the signal system. It connects an executable gate list to the mathematical block-encoding contract.
How the proof goes
Evaluate the gate list, project the ancilla-zero rows and columns, then compare the signal entries.
- Uses
QuantumBlockEncoding.CircuitMatrixSemantics;QuantumBlockEncoding.signalSystemBlockProjection- Still outside this result
- None within the declared reusable route.
Route closure
QuantumBlockEncoding.CertifiedCircuitBlockExtraction.extractionTargetQuantumBlockEncoding.CertifiedCircuitBlockExtraction.exactCleanBlockQuantumBlockEncoding.CertifiedCircuitBlockExtraction.exactCleanBlock_correct
Natural-language steps and Lean objects
| Mathematical step | Lean object or step |
|---|---|
| Evaluate syntax. | CircuitMatrixSemantics.ofGateMatrices |
| Extract the selected block. | signalSystemBlockProjection |
Open the Lean statement and source links
def CircuitMatrixSemantics.blockExtractionTarget
{α : Type u} [OfNat α 0] [OfNat α 1]
[HAdd α α α] [HMul α α α]
{qubits : Nat}
(sem : CircuitMatrixSemantics α qubits)
(dim signalDim : Nat)
(hDim : qubitDim qubits = signalDim * dim)
(targetMatrix : Matrix dim dim α)
(normalizer : α)
(signalIdx : Fin signalDim) :
BlockExtractionTarget α dim dim signalDim whereLocal declaration · Verso Blueprint · commit-pinned GitHub source
Lean result
Projected block and clean-branch action agree
QuantumBlockEncoding.ConcreteSemantics.pointwiseProjection_iff_cleanBasisAction
DeclarationCompiled
Full routeCompiled
\[\Pi U\Pi^\dagger=B\iff \langle0^a,i|U|0^a,j\rangle=B_{ij}.\]
What it says
Checking every clean projected entry is equivalent to checking the clean output amplitude after acting on every clean basis input.
Why it matters
This is the finite-matrix bridge between the projected-block definition and the action-on-a-state proof style used in circuit derivations. Readers can follow a paper's state evolution without changing the mathematical acceptance contract.
How the proof goes
Apply the matrix to a basis ket, use column selection, and identify the clean signal-system row.
- Uses
QuantumBlockEncoding.ConcreteSemantics.cleanBasisActionAmplitude;QuantumBlockEncoding.ConcreteSemantics.applyVec_basisKet- Still outside this result
- None within the finite basis-action/projection bridge.
Route closure
QuantumBlockEncoding.ConcreteSemantics.cleanBasisActionAmplitude_eq_signalSystemBlockProjectionQuantumBlockEncoding.ConcreteSemantics.pointwiseProjection_iff_cleanBasisAction
Natural-language steps and Lean objects
| Mathematical step | Lean object or step |
|---|---|
| Select one clean basis input. | applyVec_basisKet |
| Read one clean output amplitude. | cleanBasisActionAmplitude_eq_signalSystemBlockProjection |
| Quantify over both system indices. | pointwiseProjection_iff_cleanBasisAction |
Open the Lean statement and source links
theorem pointwiseProjection_iff_cleanBasisAction
{signalDim systemDim : Nat} {α : Type u} [NonAssocSemiring α]
(operator : FiniteMatrix (signalDim * systemDim) (signalDim * systemDim) α)
(signalIndex : Fin signalDim) (target : Matrix systemDim systemDim α) :
Matrix.PointwiseEq
(signalSystemBlockProjection signalDim systemDim systemDim
operator signalIndex)
target ↔
∀ output input,
cleanBasisActionAmplitude operator signalIndex output input =
target output input := byLocal declaration · Verso Blueprint · commit-pinned GitHub source