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 · proof versus engineering evidence

A correct circuit and a cheap circuit are different questions

First prove the mathematical contract. Then count gates, depth, ancillas, and oracle calls. Finally export exactly the certified gate list to Qiskit or OpenQASM for independent executable checks.

One source of truth feeds both formal and executable evidence.
circuit IR Lean-owned data resourceQiskitOpenQASM audited evidence
  1. CorrectnessLean proves the operator or state contract.
  2. CostThe resource tuple is computed from the declared circuit.
  3. ExportQiskit/OpenQASM receive the same canonical circuit.
  4. Cross-checkNumerical operator comparison can catch implementation bugs but does not replace the theorem.

Textbook / teaching anchor

Quantum circuits

IBM Quantum Learning / John Watrous

Visual circuit-model reference.

Strict mathematics, after the picture

The equations behind the intuition

\[c(U)=(g,d,a,o)\]
\[c_1\prec_{\mathrm{lex}}c_2\]

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

Textbook / teaching anchor

Quantum circuits

IBM Quantum Learning / John Watrous

Visual circuit-model reference.

Learn Lean while learning quantum computing

Lean idea: costs are data, dominance is a theorem

BlockEncodingCost.betterThan

When the site says one candidate is better, a named Lean theorem fixes the ordering and the compared tuples.

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

System and evidence · Chapter 8 of 9

Candidate comparison and executable exports

Keep formal validity lexicographically ahead of resource quality, then expose accepted candidates to executable tooling.

Lean modules used in this chapter
  • QuantumBlockEncoding/Resources.lean
  • QuantumBlockEncoding/BlockEncoding.lean
  • QuantumBlockEncoding/Automation.lean
  • QuantumBlockEncoding/PromiseGateOptimization.lean
  • QuantumBlockEncoding/CubicAmplitudePrimitive.lean

Textbook lesson

Build the idea before opening the proof

Correctness is a gate; resource quality ranks only candidates that pass it.

Lexicographic ranking

\[(g,d,a,o)_1<_{\rm lex}(g,d,a,o)_2.\]

The first differing coordinate decides. A low-depth invalid circuit never outranks a valid certificate.

Promise registers as a proved optimization rule

\[C(V^\dagger U V)=(I\otimes V^\dagger)C(U)(I\otimes V).\]

ASPBE proves the controlled-conjugation identity from arXiv:2603.12917 as an exact finite permutation-matrix theorem. The planner may remove controls from V and V-dagger only after matching register order and target semantics.

Dirty helper for an involution

\[U^2=I:\quad\mathrm{toggle};C(U);\mathrm{toggle};C(U).\]

ASPBE also proves that this protocol restores an arbitrary dirty flag and costs one extra controlled-U compared with the clean-flag construction. Concrete candidates still owe the involution, promise, restoration, and same-tier resource proofs.

Executable checks

\[\text{Lean certificate}+\text{finite export}+\text{backend report}.\]

Qiskit or QASM tests catch convention and implementation errors, but numerical agreement is not substituted for the symbolic theorem.

Check your understanding

Identify which cost coordinates are proved from the logical circuit and which depend on a selected hardware backend.

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

System and evidence: Candidate comparison and executable exports editable Mermaid source 
flowchart LR
  C["Candidate construction<br/>U"] --> F["Finite screen<br/>dimensions · unitarity · clean block"]
  F --> L{"Named Lean theorem"}
  L -- "closed" --> V["Certified construction"]
  V --> E["Optional Qiskit /<br/>OpenQASM export"]
  L -- "open" --> O["Explicit obstruction<br/>or missing proof leaf"]
  O --> R["Change construction route<br/>or one declared ε rung"]
  R --> C

  classDef math fill:#ffffff,stroke:#5b6670,color:#222222,stroke-width:1.25px;
  classDef proof fill:#ffffff,stroke:#2f7355,color:#18382b,stroke-width:1.6px;
  classDef fail fill:#ffffff,stroke:#8a5a4a,color:#4c332c,stroke-width:1.4px;
  class C,F,R math;
  class L,V,E proof;
  class O fail;

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

Control only the middle of a conjugation

QuantumBlockEncoding.PromiseGateOptimization.controlledConjugation_matrix
DeclarationCompiled Full routeCompiled
\[C(V^\dagger U V)=(I\otimes V^\dagger)\,C(U)\,(I\otimes V).\]

What it says

For a controlled V-dagger U V construction, V and V-dagger stay uncontrolled; only U receives the control.

Why it matters

Both control branches agree: the false branch cancels V with V-dagger, and the true branch performs the conjugated target. This removes expensive controls and lets the outer operations use promise-register workspace.

How the proof goes

Prove the basis action by cases on the control bit, then lift the equivalence equality to permutation matrices.

Uses
QuantumBlockEncoding.PromiseGateOptimization.controlledConjugation_equiv; QuantumBlockEncoding.Robin.ComplexLCU.equivPermutationMatrix_mul
Still outside this result
None for this local declaration.

Route closure

Natural-language steps and Lean objects

Mathematical stepLean object or step
Split the false and true control branches.cases control
Cancel the outer equivalence on the false branch.Equiv.symm_apply_apply
Compose the three permutation matrices.equivPermutationMatrix_mul
Open the Lean statement and source links 
theorem controlledConjugation_matrix
    {α : Type*} [Fintype α] [DecidableEq α]
    (outer middle : Equiv.Perm α) :
    Robin.ComplexLCU.equivPermutationMatrix (liftTargetEquiv outer.symm) *
        (Robin.ComplexLCU.equivPermutationMatrix (controlledTargetEquiv middle) *
          Robin.ComplexLCU.equivPermutationMatrix (liftTargetEquiv outer)) =
      Robin.ComplexLCU.equivPermutationMatrix
        (controlledTargetEquiv (conjugatedTargetEquiv outer middle)) := by

Local declaration · Verso Blueprint · commit-pinned GitHub source

Lean result

Replace a clean flag by a dirty flag

QuantumBlockEncoding.PromiseGateOptimization.dirtyControlledInvolution_action
DeclarationCompiled Full routeCompiled
\[U^2=I\Longrightarrow(c,b,|\psi\rangle)\mapsto(c,b,U^{[c]}|\psi\rangle).\]

What it says

If U squared is identity, compute-use-uncompute-use restores an arbitrary dirty flag and applies U exactly when requested.

Why it matters

The extra controlled-U cancels the accidental application caused by an initially set dirty flag. It turns an ancilla-saving idea into a proof obligation that the planner can check before mutating a circuit.

How the proof goes

Case-split on the requested control and unknown dirty bit; use U(U(x))=x in the two cancellation branches.

Uses
QuantumBlockEncoding.PromiseGateOptimization.dirtyControlledInvolutionEquiv; QuantumBlockEncoding.PromiseGateOptimization.dirtyControlledInvolution_unitary
Still outside this result
None for this local declaration.

Route closure

Natural-language steps and Lean objects

Mathematical stepLean object or step
Toggle the dirty flag with the predicate.toggleDirtyFlagEquiv
Use U under the flag twice.dirtyFlagControlledTargetEquiv
Apply involutivity to cancel accidental work.involutive
Read the exact clean/dirty cost tradeoff.dirtyFlag_replaces_cleanFlag
Open the Lean statement and source links 
theorem dirtyControlledInvolution_action
    {κ α : Type*} (control : κ → Bool) (target : Equiv.Perm α)
    (involutive : ∀ value, target (target value) = value)
    (key : κ) (flag : Bool) (value : α) :
    dirtyControlledInvolutionEquiv control target (key, flag, value) =
      (key, flag, if control key then target value else value) := by

Local declaration · Verso Blueprint · commit-pinned GitHub source

Lean result

Lexicographic candidate comparison

QuantumBlockEncoding.BlockEncodingCost.betterThan
DeclarationCompiled Full routeCompiled
\[c_1\prec_{\mathrm{lex}}c_2.\]

What it says

Two candidate costs are compared by a fixed, explicit priority order.

Why it matters

A smaller later metric never compensates for failing an earlier acceptance priority. Population maintenance and promotion must be reproducible across runs.

How the proof goes

Compare the first differing coordinate in the declared score tuple.

Uses
QuantumBlockEncoding.BlockEncodingCost
Still outside this result
None for this local declaration.

Route closure

Natural-language steps and Lean objects

Mathematical stepLean object or step
Build both score records.BlockEncodingCost
Apply the fixed ordering.BlockEncodingCost.betterThan
Open the Lean statement and source links 
def betterThan (x y : BlockEncodingCost) : Prop :=
  x.gateCount < y.gateCount ∨
  (x.gateCount = y.gateCount ∧
    (x.depth < y.depth ∨
      (x.depth = y.depth ∧
        (x.auxiliaryQubits < y.auxiliaryQubits ∨
          (x.auxiliaryQubits = y.auxiliaryQubits ∧
            x.oracleCalls < y.oracleCalls)))))

/-- Non-strict version for accepting a candidate as no worse than a baseline. -/

Local declaration · Verso Blueprint · commit-pinned GitHub source

Lean result

Finite cubic amplitude oracle

QuantumBlockEncoding.CubicDiagonalOracle.cubicN2PrimitiveVerifiedBlockEncoding
DeclarationCompiled Full routeCompiled
\[\Pi_0U_{\mathrm{cubic},2}\Pi_0^\dagger=\operatorname{diag}(0,(1/4)^3,(2/4)^3,(3/4)^3).\]

What it says

A four-way uniformly controlled RY circuit exactly block-encodes the two-qubit cubic diagonal operator.

Why it matters

Each system basis string selects the exact angle 2 arccos((j/4)^3); the clean RY entry is therefore the desired diagonal amplitude. The earlier opaque one-call tuple remains a diagnostic, but the accepted teaching route now has gate-expanded semantics, exact clean projection, and a verified block-encoding wrapper.

How the proof goes

Compile the four exact amplitudes through the uniformly controlled RY theorem, prove the clean entries, reindex the little-endian basis, and package the resulting unitary as a verified block encoding.

Uses
QuantumBlockEncoding.compileUniformlyControlledRy_eval_controlledRyBlockMatrix; QuantumBlockEncoding.CubicDiagonalOracle.cubicN2PrimitiveProgram_cleanEntry; QuantumBlockEncoding.CubicDiagonalOracle.cubicN2PrimitiveFlatUnitary_unitary
Still outside this result
None within the fixed n=2 primitive route. Scalable arithmetic and general QSVT phase synthesis remain separately scoped research routes.

Route closure

Natural-language steps and Lean objects

Mathematical stepLean object or step
Select one exact cubic amplitude.cubicN2Angle
Compile the multiplexed rotations.cubicN2PrimitiveCircuit_eval
Prove the clean diagonal entry.cubicN2PrimitiveProgram_cleanEntry
Promote the flat unitary and block.cubicN2PrimitiveVerifiedBlockEncoding
Open the Lean statement and source links 
noncomputable def cubicN2PrimitiveVerifiedBlockEncoding :
    VerifiedOperatorBlockEncoding ℂ 2 where
  candidate := cubicN2PrimitiveOperatorCandidate
  unitaryProof := cubicN2PrimitiveFlatUnitary_unitary
  blockProof := by

Local declaration · Verso Blueprint · commit-pinned GitHub source