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

State preparation · two exact typed circuits + same-target resource theorem

Structured probability loading: product structure beats the generic tree

Prepare amplitudes (9,12,12,16)/25, whose probabilities come from two identical Bernoulli factors. Compare the generic recursive tree with the circuit obtained by exposing product structure.

Lean certifiedA structured probability-loading example shows how ASPBE can preserve the exact state while removing conditional structure and reducing certified resources.

Source paper · paper-derived structured finite benchmark

Where this example comes from

Creating superpositions that correspond to efficiently integrable probability distributions
Lov Grover, Terry Rudolph · 2002

Source anchor. Grover–Rudolph Eq. (1), (3), (6)

Eq. (1) Eq. (3) Eq. (6)

What the paper says. Eq. (1) is the target probability-amplitude state, Eq. (3) is the recursive one-qubit refinement, and Eq. (6) realizes that refinement by a controlled rotation after coherently computing the split angle.

What ASPBE does here. ASPBE chooses a two-bit product distribution as an exact finite specialization. The factorized two-rotation winner is an ASPBE same-target optimization; it is not stated as a resource theorem in the source paper.

Open source paper ↗

Read this before the proof dashboard

Learn when structure in a probability distribution should remove conditional circuitry rather than merely alter angles.

The four amplitudes factor into two identical one-qubit amplitude pairs. A generic binary tree is correct but needlessly conditional; the factorized route exposes two parallel rotations.

Grover–Rudolph prepares states corresponding to efficiently integrable probability distributions. This finite product instance isolates the structural optimization while leaving the general integration/oracle machinery in Papers.

Read the circuit

What the wires and stages are doing

1
Generic tree

Root RY followed by one-control UCRY gives a proof-bearing five-gate route.

2
Spot the tensor product

Every amplitude is a product of 3/5 and 4/5.

3
Remove the conditional

Prepare q0 and q1 independently.

4
Parallelize

The two RY gates touch different wires, so depth is one.

5
Compare after correctness

Both routes first prove the same state action, then betterThan compares costs.

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

Correctness theorem

Both typed circuits prepare the same exact product state

\[U|00\rangle=(9|00\rangle+12|01\rangle+12|10\rangle+16|11\rangle)/25\]

Lean checks the exact target and proves state action for the generic tree and factorized circuit.

Proof story

  1. Normalize one factor(3/5)^2+(4/5)^2=1.
  2. TensorThe four amplitudes are 9,12,12,16 over 25.
  3. Evaluate factorized routeTwo lifted RY matrices give the explicit product matrix.
  4. Reduce generic treeConstant UCRY is exactly the same single-wire RY semantics.
  5. Package routesBoth become ExactPrimitiveStatePreparationRoute values.
Show the Lean proof checkpoints

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

What ASPBE improves

Exploit product structure instead of paying for a conditional tree

\[(2,1,0,0)\prec_{\mathrm{lex}}(5,4,0,0)\]

The factorized typed circuit uses two parallel rotations; the generic typed UCRY route uses five gates at depth four. The comparison theorem is downstream of exact state-action proofs.

Why the proof is allowed to say “better”

  1. Freeze the targetBoth routes prepare exactly the same amplitudes.
  2. Compute tree resourcesThe typed root-RY/UCRY route yields (5,4,0,0).
  3. Compute factorized resourcesTwo disjoint RY gates yield (2,1,0,0).
  4. Apply lexicographic order2<5 closes strict dominance already on gate count.
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{prod}}\rangle=\left(\frac35|0\rangle+\frac45|1\rangle\right)\otimes\left(\frac35|0\rangle+\frac45|1\rangle\right)=\frac{9|00\rangle+12|01\rangle+12|10\rangle+16|11\rangle}{25}.\]

Lean proves both typed primitive circuits prepare the same exact target. The generic root-RY plus one-control-UCRY circuit has cost (5,4,0,0); the factorized circuit contains two independent RY gates, cost (2,1,0,0). A named betterThan theorem certifies strict lexicographic improvement.

Eq. (1)
Grover–Rudolph's probability-amplitude target state
Eq. (3), Eq. (6)
the recursive refinement and controlled-rotation mechanism
betterThan
ASPBE's fixed lexicographic order: gates, depth, auxiliary qubits, oracle calls

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; no ancilla
01

Generic tree

root split followed by a one-control conditional split

RYRYCXRYCX
02

Use factorization

two independent identical RY rotations act on disjoint wires

RY(q0) || RY(q1)

Auditable evolution

Candidate and proof progression

Both points are proof-bearing typed circuits for the same target; only then is the resource comparison allowed.

iteration0

Generic binary tree

Lean certified

Correct but structure-blind root plus UCRY route.

Generic binary treeq_1:ket0R_y(2arccos(3/5))q_0:ket0R_yR_y
Grouped-register circuit. Open the source or workbench to adapt notation.
Lean rootQuantumBlockEncoding.StatePreparationBenchmarks.groverRudolphTreeVerified_cost Edit and preview this stage →
Copy this stage as quantikz 
\begin{quantikz}[row sep=.4cm,column sep=.45cm]
\lstick{$q_1:\ket0$} & \gate{R_y(2\arccos(3/5))} & \ctrl{1} & \qw & \ctrl{1} & \qw \\
\lstick{$q_0:\ket0$} & \qw & \gate{R_y} & \targ{} & \gate{R_y} & \targ{}
\end{quantikz}
5gates4depth0aux0oracles
iteration1

Factorized product route

Strictly better · Lean certified

Factorization removes conditional branching and exposes two parallel rotations.

Factorized product routeq_0:ket0R_y(2arccos(3/5))q_1:ket0R_y(2arccos(3/5))
Grouped-register circuit. Open the source or workbench to adapt notation.
Lean rootQuantumBlockEncoding.StatePreparationBenchmarks.groverRudolphFactorized_betterThan_tree Edit and preview this stage →
Copy this stage as quantikz 
\begin{quantikz}[row sep=.4cm,column sep=.65cm]
\lstick{$q_0:\ket0$} & \gate{R_y(2\arccos(3/5))} & \qw \\
\lstick{$q_1:\ket0$} & \gate{R_y(2\arccos(3/5))} & \qw
\end{quantikz}
2gates1depth0aux0oracles

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{prod}}\rangle=\left(\frac35|0\rangle+\frac45|1\rangle\right)\otimes\left(\frac35|0\rangle+\frac45|1\rangle\right)=\frac{9|00\rangle+12|01\rangle+12|10\rangle+16|11\rangle}{25}.
\]

% Generic binary tree
\begin{quantikz}[row sep=.4cm,column sep=.45cm]
\lstick{$q_1:\ket0$} & \gate{R_y(2\arccos(3/5))} & \ctrl{1} & \qw & \ctrl{1} & \qw \\
\lstick{$q_0:\ket0$} & \qw & \gate{R_y} & \targ{} & \gate{R_y} & \targ{}
\end{quantikz}

% Factorized product route
\begin{quantikz}[row sep=.4cm,column sep=.65cm]
\lstick{$q_0:\ket0$} & \gate{R_y(2\arccos(3/5))} & \qw \\
\lstick{$q_1:\ket0$} & \gate{R_y(2\arccos(3/5))} & \qw
\end{quantikz}
    English proof LaTeX 
    \paragraph{Proof.}
Lean proves both typed primitive circuits prepare the same exact target. The generic root-RY plus one-control-UCRY circuit has cost (5,4,0,0); the factorized circuit contains two independent RY gates, cost (2,1,0,0). A named betterThan theorem certifies strict lexicographic improvement.
\begin{enumerate}
  \item Correct but structure-blind root plus UCRY route.
  \item Factorization removes conditional branching and exposes two parallel rotations.
\end{enumerate}
Each advertised certificate is the named Lean declaration linked on this page.
    Lean declaration retrieval block 
    import QuantumBlockEncoding

#check QuantumBlockEncoding.StatePreparationBenchmarks.groverRudolphProductTarget_normalized
#check QuantumBlockEncoding.StatePreparationBenchmarks.groverRudolphProductMatrix_unitary
#check QuantumBlockEncoding.StatePreparationBenchmarks.groverRudolphFactorized_prepares_target
#check QuantumBlockEncoding.StatePreparationBenchmarks.groverRudolphTree_prepares_target
#check QuantumBlockEncoding.StatePreparationBenchmarks.groverRudolphTreeVerified_cost
#check QuantumBlockEncoding.StatePreparationBenchmarks.groverRudolphFactorizedVerified_cost
#check QuantumBlockEncoding.StatePreparationBenchmarks.groverRudolphFactorized_betterThan_tree
    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 factorized winner; Lean proves both candidate semantics and the resource ordering.

    Current runnable artifact
    executable-exports/SP-PAPERS-001/qiskit/export.py
    Command
    python3 executable-exports/SP-PAPERS-001/qiskit/export.py --case grover-rudolph
    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
    Grover–Rudolph Eq. (1), Eq. (3), Eq. (6), arXiv:quant-ph/0208112
    Contributor
    ASPBE authors
    Current boundary
    This is a finite product-distribution witness. The general efficiently-integrable distribution theorem and integration/arithmetic oracle compiler remain in Papers.
    Load in task builderContribute a variant