QuantumComputinglib learn · inspect · formalize
Checked on this commit 2,822 public declarations commit 07559c3d051f Build record

Block encoding · exact finite logical reversible circuit

BE Case 1: finite transfer operator

Encode the non-unitary transfer that moves the time/type label (1,1) to (0,0) while leaving the state bit unchanged.

Lean certifiedA concrete non-unitary transfer is embedded in a permutation unitary and improved from (6,5,1,0) to (4,2,1,0).

Read this before the proof dashboard

Understand why a non-unitary map needs a larger unitary before a quantum circuit can implement it.

The transfer E1 maps one labelled sector of the system into another and is not itself a unitary gate. The case shows the basic block-encoding trick without hiding behind a large oracle: add one clean signal qubit and complete the desired action to a reversible permutation.

This is the finite toy model for the general situation in scientific computing: the linear map you care about is often not unitary, while the quantum circuit must be.

Read the circuit

What the wires and stages are doing

1
System registers

Three qubits carry time, type, and a passive state label.

2
Signal ancilla

One extra qubit makes enough room for a reversible completion.

3
Clean branch

When the signal starts and ends at 0, the system block equals E1.

4
Other branch

The remaining basis states are filled in only to make the full map bijective/unitary.

The detailed circuit diagrams generated from the case record appear below this tutorial.

Statement → proof → optional Lean

The mathematical claims, in the order a human would prove them

Case theorem

The clean ancilla block equals the finite transfer operator

\[E_1=|0\rangle\!\langle1|_{t}\otimes|0\rangle\!\langle1|_{y}\otimes I_2,\qquad \langle0|_aU|0\rangle_a=E_1\]

The constructed full basis map is a permutation, hence unitary, and every clean-block matrix entry agrees with E1 exactly with alpha=1.

Proof story

  1. Specify the desired partial actionOnly the labelled input sector (t,y)=(1,1) should move to (0,0); the passive state bit is unchanged.
  2. Complete it reversiblyUse the signal qubit to route collisions into the complementary branch so the full basis map is bijective.
  3. Lift the bijection to a unitaryA finite permutation of basis states gives a permutation matrix.
  4. Project the clean blockFix signal input/output to 0 and check the remaining 8 by 8 block equals E1.
Show the Lean proof checkpoints

The mathematical explanation above is the reading layer. These compiled declarations are the proof authority.

What ASPBE improves

The same exact operator with a shallower reversible circuit

\[(6,5,1,0)\;\succ\;(4,4,1,0)\;\succ\;(4,2,1,0)\]

Under one frozen logical gate convention and the lexicographic score (gate count, depth, auxiliary qubits, oracle calls), Lean proves two strict improvements while the clean block stays unchanged.

Why the proof is allowed to say “better”

  1. First reductionRemove redundant gates from the direct completion and re-prove the same permutation and clean block.
  2. ParallelizeRewrite the final candidate so three X operations occupy one parallel layer after a Toffoli.
  3. Recompute resourcesThe score is derived from the declared circuit/schedule rather than typed by hand.
  4. Compare in LeanThe betterThan theorems prove strict lexicographic dominance only after correctness has already passed.
Show the Lean winner/comparison theorems

The mathematical explanation above is the reading layer. These compiled declarations are the proof authority.

Mathematical target

The equation being studied

\[E_1=|0\rangle\!\langle1|_{\mathrm{time}}\otimes|0\rangle\!\langle1|_{\mathrm{type}}\otimes I_2,\qquad \langle0|_aU|0\rangle_a=E_1.\]

The system has time, type, and state qubits. One clean signal qubit enlarges E_1 to a permutation unitary. Lean proves the full permutation/orthogonality property and every clean-block entry exactly with alpha=1.

E_1
the concrete 8 by 8 transfer operator
a
the one-qubit clean signal register
I_2
identity on the passive state qubit

Circuit anatomy

How the candidate acts

These blocks show logical stages and register responsibilities. They do not pretend an unresolved logical oracle is already a primitive hardware gate.

Register ordersignal a | time t | type y | passive state s
01

Generation 0

expanded depth-5 completion

XCNOTCNOTCNOTToffoliX
02

Generation 1

equality flag then transfer

XCNOTCNOTToffoli
03

Generation 2

one Toffoli then three parallel X gates

ToffoliX || X || X

Auditable evolution

Candidate and proof progression

All three points are exact Lean-certified block encodings in one logical gate convention. Both arrows are Lean theorems about the fixed lexicographic order.

iteration0

Depth-5 completion

Lean certified

A direct reversible completion establishes the first accepted point.

Depth-5 completiona:ket0Xtys
Grouped-register circuit. Open the source or workbench to adapt notation.
Lean rootQuantumBlockEncoding.OptimalControl.reducedDepth5Verified Edit and preview this stage →
Copy this stage as quantikz 
\begin{quantikz}[row sep=.35cm, column sep=.3cm]
\lstick{$a:\ket0$} & \gate{X} & \ctrl{1} & \ctrl{2} & \targ{} & \qw \\
\lstick{$t$}        & \qw      & \targ{}  & \qw      & \ctrl{-1}& \qw \\
\lstick{$y$}        & \qw      & \qw      & \targ{}  & \ctrl{-2}& \qw \\
\lstick{$s$}        & \qw      & \qw      & \qw      & \qw      & \qw
\end{quantikz}
6gates5depth1aux0oracles
iteration1

Equality-transfer

Strictly better

Two gates are removed while preserving the exact clean block.

Equality-transfera:ket0Xtys
Grouped-register circuit. Open the source or workbench to adapt notation.
Lean rootQuantumBlockEncoding.OptimalControl.proEqTransferCost_betterThan_depth5 Edit and preview this stage →
Copy this stage as quantikz 
\begin{quantikz}[row sep=.35cm, column sep=.4cm]
\lstick{$a:\ket0$} & \gate{X} & \ctrl{1} & \ctrl{2} & \targ{} & \qw \\
\lstick{$t$}        & \qw      & \targ{}  & \qw      & \ctrl{-1}& \qw \\
\lstick{$y$}        & \qw      & \qw      & \targ{}  & \ctrl{-2}& \qw \\
\lstick{$s$}        & \qw      & \qw      & \qw      & \qw      & \qw
\end{quantikz}
4gates4depth1aux0oracles
iteration2

Parallel equality-flip

Strictly better

Gate count ties the previous candidate and parallel depth falls from four to two.

Parallel equality-flipa:ket0XtXyXs
Grouped-register circuit. Open the source or workbench to adapt notation.
Lean rootQuantumBlockEncoding.OptimalControl.evolvedEqFlipCost_betterThan_pro Edit and preview this stage →
Copy this stage as quantikz 
\begin{quantikz}[row sep=.35cm, column sep=.55cm]
\lstick{$a:\ket0$} & \ctrl{1} & \gate{X} & \qw \\
\lstick{$t$}        & \ctrl{1} & \gate{X} & \qw \\
\lstick{$y$}        & \targ{}  & \gate{X} & \qw \\
\lstick{$s$}        & \qw      & \qw      & \qw
\end{quantikz}
4gates2depth1aux0oracles

Reader workbench

Edit, preview, then copy

Change symbols, language, proof steps, or the grouped-register circuit locally in your browser. The preview is explanatory; the linked Lean declaration remains the certificate.

Mathematical construction

Proof steps

One step per line. Natural language and inline mathematics are both accepted.

    Quantum circuit

    Complete packet

    Copy the reviewed construction and proof

    The packet below is generated from the reviewed case record. The exact primitive authority is the linked Lean source and executable artifact.

    Construction and circuit LaTeX 
    % Requires: \usepackage{quantikz}
\paragraph{Construction.}
\[
E_1=|0\rangle\!\langle1|_{\mathrm{time}}\otimes|0\rangle\!\langle1|_{\mathrm{type}}\otimes I_2,\qquad \langle0|_aU|0\rangle_a=E_1.
\]

% Depth-5 completion
\begin{quantikz}[row sep=.35cm, column sep=.3cm]
\lstick{$a:\ket0$} & \gate{X} & \ctrl{1} & \ctrl{2} & \targ{} & \qw \\
\lstick{$t$}        & \qw      & \targ{}  & \qw      & \ctrl{-1}& \qw \\
\lstick{$y$}        & \qw      & \qw      & \targ{}  & \ctrl{-2}& \qw \\
\lstick{$s$}        & \qw      & \qw      & \qw      & \qw      & \qw
\end{quantikz}

% Equality-transfer
\begin{quantikz}[row sep=.35cm, column sep=.4cm]
\lstick{$a:\ket0$} & \gate{X} & \ctrl{1} & \ctrl{2} & \targ{} & \qw \\
\lstick{$t$}        & \qw      & \targ{}  & \qw      & \ctrl{-1}& \qw \\
\lstick{$y$}        & \qw      & \qw      & \targ{}  & \ctrl{-2}& \qw \\
\lstick{$s$}        & \qw      & \qw      & \qw      & \qw      & \qw
\end{quantikz}

% Parallel equality-flip
\begin{quantikz}[row sep=.35cm, column sep=.55cm]
\lstick{$a:\ket0$} & \ctrl{1} & \gate{X} & \qw \\
\lstick{$t$}        & \ctrl{1} & \gate{X} & \qw \\
\lstick{$y$}        & \targ{}  & \gate{X} & \qw \\
\lstick{$s$}        & \qw      & \qw      & \qw
\end{quantikz}
    English proof LaTeX 
    \paragraph{Proof.}
The system has time, type, and state qubits. One clean signal qubit enlarges E_1 to a permutation unitary. Lean proves the full permutation/orthogonality property and every clean-block entry exactly with alpha=1.
\begin{enumerate}
  \item A direct reversible completion establishes the first accepted point.
  \item Two gates are removed while preserving the exact clean block.
  \item Gate count ties the previous candidate and parallel depth falls from four to two.
\end{enumerate}
Each advertised certificate is the named Lean declaration linked on this page.
    Lean declaration retrieval block 
    import QuantumBlockEncoding

#check QuantumBlockEncoding.OptimalControl.reducedDepth5Verified
#check QuantumBlockEncoding.OptimalControl.proEqTransferVerified
#check QuantumBlockEncoding.OptimalControl.evolvedEqFlipVerified
#check QuantumBlockEncoding.OptimalControl.reducedDepth5Candidate_cost
#check QuantumBlockEncoding.OptimalControl.proEqTransferCandidate_cost
#check QuantumBlockEncoding.OptimalControl.evolvedEqFlipCandidate_cost
#check QuantumBlockEncoding.OptimalControl.proEqTransferCost_betterThan_depth5
#check QuantumBlockEncoding.OptimalControl.evolvedEqFlipCost_betterThan_pro
    Show the complete Lean certificate list

    Open this when you want to inspect every declaration linked to the case.

    Proof authority

    Named Lean certificates

    These declarations, compiled by the current Lean gate, support the mathematical and resource claims above.

    Optional executable checks and outputs

    Executable verification and exports

    Checking and artifact selection are independent. A user may screen with Qiskit, OpenQASM round-trip, both, or neither, then request a different set of output files.

    Backend / artifactRoleStatusEvidence
    Internal canonical evaluatorReference semantics for primitive canonical IRopenmetrics manifest
    Qiskit OperatorGate-by-gate numerical screeningartifact availableexecutable-exports/QBE-OP-OPTCTRL-001/qiskit/export.py
    OpenQASM 3 round-tripStrict serialization, import, and semantic replaynot recordedQASM and report when generated
    Lean certificateExact proof authority at the page's stated semantic tierpassed8 named root(s)

    Exports the final certified logical construction to Qiskit. Lean, not Qiskit matrix comparison, proves acceptance and the score ordering.

    Current runnable artifact
    executable-exports/QBE-OP-OPTCTRL-001/qiskit/export.py
    Command
    python3 executable-exports/QBE-OP-OPTCTRL-001/qiskit/export.py
    Trust boundary. Fast executable checks may reject, rank, or queue a route for formalization. Floating-point tolerances do not replace the exact Lean roots above; an external exact certificate contributes only after a Lean checker verifies it.
    Source
    ASPBE BE Case 1
    Contributor
    ASPBE authors
    Current boundary
    The comparison is for the declared finite logical {X, CNOT, Toffoli} convention, not a hardware-global optimum.
    Load in task builderContribute a variant