QuantumComputinglib learn · inspect · formalize
Checked on this commit 4,524 public declarations commit ab8f277c5704 Build record

State preparation · exact d=3 target + two exact typed same-target circuits

Sparse state preparation: prune the zero branches

Prepare a three-qubit state with only d=3 nonzero amplitudes, (3|000>+4|010>+12|100>)/13, and make the savings from a known-zero amplitude layer explicit.

Lean certifiedA finite Li–Luo Eq. (2) witness isolates the mechanism behind sparse preparation: remove a provably identity zero-amplitude subtree while preserving exact state semantics.

Source paper · paper-derived sparse finite benchmark

Where this example comes from

Nearly Optimal Circuit Size for Sparse Quantum State Preparation
Lvzhou Li, Jingquan Luo · 2025

Source anchor. Li–Luo Eq. (1)–(2)

Eq. (1) Eq. (2)

What the paper says. Eq. (1) represents a d-sparse state by its nonzero amplitudes and basis labels. Eq. (2) is the exact unitary preparation contract, including clean ancillary qubits.

What ASPBE does here. ASPBE sets n=3 and d=3 and proves one exact finite witness of Eq. (2). The 5-vs-15 zero-branch pruning comparison is a finite ASPBE benchmark and is not presented as a reproduction of the paper's asymptotic Theorem 1.

Open source paper ↗

Read this before the proof dashboard

See sparsity as a missing amplitude subtree that can be removed from an exact typed circuit.

Only basis indices 0,2,4 carry amplitude. A structure-blind amplitude tree can spend gates compiling a final q0 layer even though q0 is known to remain zero on all support points.

Li–Luo studies sparse-state circuit complexity asymptotically. ASPBE starts with an exact n=3,d=3 witness of Eq. (2), then makes one finite pruning mechanism machine-checkable without claiming Theorem 1.

Read the circuit

What the wires and stages are doing

1
Mark support

Only 0,2,4 are nonzero; q0 is zero on every supported basis state.

2
Prepare root

RY on q2 creates masses 5/13 and 12/13.

3
Split only the q2=0 branch

One-control UCRY on q1 produces 3/13 and 4/13; the q2=1 branch uses zero angle.

4
Define a same-target dense baseline

Append a two-control zero-angle UCRY on q0; Lean proves its exact matrix is identity.

5
Prune

Remove that identity subtree and compare the circuit-derived tuples.

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

Sparse finite theorem

The n=3,d=3 Li–Luo Eq. (2) witness has an exact typed preparation route

\[U|000\rangle=(3|000\rangle+4|010\rangle+12|100\rangle)/13\]

Lean checks exact normalization, full-unitary completion, the pruned typed circuit state action, and the same-target dense baseline.

Proof story

  1. Normalize3^2+4^2+12^2=13^2.
  2. Prepare rootUse the 5-12-13 split on q2.
  3. Prepare nonzero branchUse the 3-4-5 split on q1 when q2=0.
  4. Prove zero-fill identityA two-control UCRY with every angle zero evaluates exactly to identity.
  5. Package both routesBoth circuits therefore prepare the same target.
Show the Lean proof checkpoints

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

What ASPBE improves

Prune the provably identity zero-amplitude layer

\[(5,4,0,0)\prec_{\mathrm{lex}}(15,13,0,0)\]

The dense reference compiler spends ten extra gates on a two-control zero-angle UCRY whose semantics is exactly identity. Removing it preserves the state and strictly improves the resource tuple.

Why the proof is allowed to say “better”

  1. Freeze the sparse targetBoth circuits are already exact state-preparation routes.
  2. Count dense baselinePruned route plus the identity UCRY yields (15,13,0,0).
  3. Count pruned routeRoot plus one-control UCRY yields (5,4,0,0).
  4. Apply betterThan5<15 proves strict lexicographic improvement.
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

\[|\psi_{\mathrm{sparse}}\rangle=\frac{3|000\rangle+4|010\rangle+12|100\rangle}{13},\qquad d=3.\]

Lean proves exact normalization and a full 8 by 8 unitary completion. The pruned typed circuit uses a q2 root RY followed by a q2-controlled UCRY on q1 and has cost (5,4,0,0). The same-target dense baseline appends a two-control zero-angle UCRY on q0; Lean proves that appended block is exactly identity but its reference compiler still costs ten gates, yielding (15,13,0,0).

d-sparse
only d computational-basis amplitudes are nonzero
Eq. (2)
Li–Luo's exact preparation-unitary contract, specialized here to n=3,d=3
zero-fill baseline
a semantic identity circuit that deliberately pays for the amplitude subtree known to be zero

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 orderq0 | q1 | q2; no ancilla at this primitive tier
01

Dense zero-fill baseline

prepare the sparse target correctly, then compile a two-control zero-angle UCRY on q0

pruned 5-gate route+ 10-gate identity UCRY
02

Prune zero support

q0 remains zero; only root q2 split and q2-controlled q1 split are needed

RYRYCXRYCX

Auditable evolution

Candidate and proof progression

Both candidates are exact typed circuits preparing the same d=3 target. The asymptotic Li–Luo Theorem 1 remains outside this finite comparison.

iteration0

Dense three-qubit tree

Lean certified

Same-target baseline retains an exact-identity zero-angle amplitude layer.

Dense three-qubit treeq_2R_yq_1UCRY_1q_0UCRY_2(0)
Grouped-register circuit. Open the source or workbench to adapt notation.
Lean rootQuantumBlockEncoding.StatePreparationBenchmarks.sparseDenseTreeVerified_cost Edit and preview this stage →
Copy this stage as quantikz 
\begin{quantikz}[row sep=.35cm,column sep=.45cm]
\lstick{$q_2$} & \gate{R_y} & \ctrl{1} & \qw & \qw \\
\lstick{$q_1$} & \qw & \gate{\mathrm{UCRY}_1} & \qw & \ctrl{1} \\
\lstick{$q_0$} & \qw & \qw & \qw & \gate{\mathrm{UCRY}_2(0)}
\end{quantikz}
15gates13depth0aux0oracles
iteration1

Sparse pruned tree

Strictly better · Lean certified

The known-zero q0 amplitude layer is removed without changing the prepared state.

Sparse pruned treeq_2:ket0R_y(2arccos(5/13))q_1:ket0R_yR_yq_0:ket0
Grouped-register circuit. Open the source or workbench to adapt notation.
Lean rootQuantumBlockEncoding.StatePreparationBenchmarks.sparsePruned_betterThan_denseTree Edit and preview this stage →
Copy this stage as quantikz 
\begin{quantikz}[row sep=.35cm,column sep=.55cm]
\lstick{$q_2:\ket0$} & \gate{R_y(2\arccos(5/13))} & \ctrl{1} & \qw & \ctrl{1} & \qw \\
\lstick{$q_1:\ket0$} & \qw & \gate{R_y} & \targ{} & \gate{R_y} & \targ{} \\
\lstick{$q_0:\ket0$} & \qw & \qw & \qw & \qw & \qw
\end{quantikz}
5gates4depth0aux0oracles

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.}
\[
|\psi_{\mathrm{sparse}}\rangle=\frac{3|000\rangle+4|010\rangle+12|100\rangle}{13},\qquad d=3.
\]

% Dense three-qubit tree
\begin{quantikz}[row sep=.35cm,column sep=.45cm]
\lstick{$q_2$} & \gate{R_y} & \ctrl{1} & \qw & \qw \\
\lstick{$q_1$} & \qw & \gate{\mathrm{UCRY}_1} & \qw & \ctrl{1} \\
\lstick{$q_0$} & \qw & \qw & \qw & \gate{\mathrm{UCRY}_2(0)}
\end{quantikz}

% Sparse pruned tree
\begin{quantikz}[row sep=.35cm,column sep=.55cm]
\lstick{$q_2:\ket0$} & \gate{R_y(2\arccos(5/13))} & \ctrl{1} & \qw & \ctrl{1} & \qw \\
\lstick{$q_1:\ket0$} & \qw & \gate{R_y} & \targ{} & \gate{R_y} & \targ{} \\
\lstick{$q_0:\ket0$} & \qw & \qw & \qw & \qw & \qw
\end{quantikz}
    English proof LaTeX 
    \paragraph{Proof.}
Lean proves exact normalization and a full 8 by 8 unitary completion. The pruned typed circuit uses a q2 root RY followed by a q2-controlled UCRY on q1 and has cost (5,4,0,0). The same-target dense baseline appends a two-control zero-angle UCRY on q0; Lean proves that appended block is exactly identity but its reference compiler still costs ten gates, yielding (15,13,0,0).
\begin{enumerate}
  \item Same-target baseline retains an exact-identity zero-angle amplitude layer.
  \item The known-zero q0 amplitude layer is removed without changing the prepared state.
\end{enumerate}
Each advertised certificate is the named Lean declaration linked on this page.
    Lean declaration retrieval block 
    import QuantumBlockEncoding

#check QuantumBlockEncoding.StatePreparationBenchmarks.sparseThreeTarget_normalized
#check QuantumBlockEncoding.StatePreparationBenchmarks.sparseThreeMatrix_unitary
#check QuantumBlockEncoding.StatePreparationBenchmarks.sparsePruned_prepares_target
#check QuantumBlockEncoding.StatePreparationBenchmarks.sparseDenseTree_prepares_target
#check QuantumBlockEncoding.StatePreparationBenchmarks.sparseDenseTreeVerified_cost
#check QuantumBlockEncoding.StatePreparationBenchmarks.sparsePrunedVerified_cost
#check QuantumBlockEncoding.StatePreparationBenchmarks.sparsePruned_betterThan_denseTree
    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 replayGate-by-gate numerical screeningartifact availableexecutable-exports/SP-PAPERS-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 tierpassed7 named root(s)

    Numerically mirrors the pruned exact route; Lean proves the exact target and same-target resource comparison.

    Current runnable artifact
    executable-exports/SP-PAPERS-001/qiskit/export.py
    Command
    python3 executable-exports/SP-PAPERS-001/qiskit/export.py --case sparse
    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
    Li–Luo Eq. (1)–(2), arXiv:2406.16142
    Contributor
    ASPBE authors
    Current boundary
    Fixed n=3,d=3 witness only. The asymptotic sparse constructions, ancilla tradeoffs, and Theorem 1 lower/upper bounds remain in Papers.
    Load in task builderContribute a variant