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

State preparation · exact dense target + exact typed root-RY/UCRY circuit

Dense real-amplitude preparation: a Möttönen-style two-qubit benchmark

Prepare the genuinely dense non-product real state with amplitudes (39,52,60,144)/169 and expose the recursive uniformly-controlled-rotation architecture used by dense state synthesis.

Lean certifiedA non-product dense state links the first-column contract to Möttönen's UCRY recursion using an exact proof-bearing primitive circuit.

Source paper · paper-derived finite benchmark

Where this example comes from

Transformation of quantum states using uniformly controlled rotations
Mikko Möttönen, Juha J. Vartiainen, Ville Bergholm, Martti M. Salomaa · 2005

Source anchor. Möttönen et al. Eq. (6)–(8) + Fig. 3

Eq. (6) Eq. (7) Eq. (8) Fig. 3

What the paper says. Eq. (6) shows one uniformly controlled y-rotation eliminating one qubit, Eq. (7) composes the recursive preparation route, Eq. (8) gives the rotation angles, and Fig. 3 displays the resulting state-preparation circuit.

What ASPBE does here. ASPBE instantiates this UCRY architecture on one exact two-qubit dense real-amplitude target. The finite target/unitary proof is certified; the paper-wide arbitrary-n gate-count theorem is not claimed reproduced.

Open source paper ↗

Read this before the proof dashboard

See how Möttönen's recursive UCRY architecture becomes a fully exact finite typed-circuit certificate.

A dense non-product target has no sparse or tensor-product shortcut. The nested-Pythagorean amplitudes make every finite rotation exact while retaining the generic binary-tree structure.

Dense amplitude loading is a front-end cost for many amplitude-encoded algorithms. Möttönen et al. supply a general UCRY state-synthesis architecture; ASPBE closes one exact two-qubit instantiation.

Read the circuit

What the wires and stages are doing

1
Root split

RY on q1 sets total branch masses 5/13 and 12/13.

2
Conditional split

One-control UCRY on q0 selects the 3/5,4/5 or 5/13,12/13 branch pair.

3
Read clean columns

Only the two columns populated by the root state are needed to prove exact action.

4
Count the typed route

The compiler emits 5 gates with parallel depth 4.

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

Finite paper benchmark

Möttönen Eq. (6)–(8)/Fig. 3 has an exact two-qubit typed instantiation

\[U|00\rangle=(39|00\rangle+52|01\rangle+60|10\rangle+144|11\rangle)/169\]

Lean certifies normalization, a full unitary completion, the typed root-RY/UCRY state action, and cost (5,4,0,0).

Proof story

  1. Normalize39^2+52^2+60^2+144^2=169^2.
  2. Root split5-12-13 gives the exact first RY.
  3. Conditional branches3-4-5 and 5-12-13 give exact branch rotations.
  4. Use UCRY semanticsThe reference compiler equals its controlled block-diagonal specification.
  5. Compose and countThe exact typed circuit prepares the target and supplies the resource tuple.
Show the Lean proof checkpoints

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

Mathematical target

The equation being studied

\[|\psi_{\mathrm{dense}}\rangle=\frac{39|00\rangle+52|01\rangle+60|10\rangle+144|11\rangle}{169}.\]

The target is an exact nested-Pythagorean instance: the root split uses 5/13 and 12/13, while the two conditional branches use 3/5,4/5 and 5/13,12/13. Lean proves target normalization, a full unitary completion, the exact typed root-RY plus one-control-UCRY state action, and circuit-derived cost (5,4,0,0).

UCRY
a uniformly controlled y rotation whose target angle depends coherently on the control state
Eq. (8)
Möttönen et al.'s rotation-angle recursion used by the paper architecture
(39,52,60,144)/169
an exact finite target chosen so all preparation angles have Pythagorean closed forms

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

Root probability split

RY on q1 sets branch masses 5/13 and 12/13

RY(q1; 5/13,12/13)
02

Conditional amplitudes

one-control UCRY on q0 resolves 3/5,4/5 in q1=0 and 5/13,12/13 in q1=1

RYCXRYCX

Auditable evolution

Candidate and proof progression

This is a finite instantiation of Möttönen Eq. (6)–(8)/Fig. 3. The arbitrary-n synthesis theorem remains a Papers reproduction task.

iteration0

Dense UCRY tree

Lean certified

The same typed five-gate circuit supplies exact state action and parallel depth four.

Dense UCRY treeq_1:ket0R_y(2arccos(5/13))q_0:ket0R_yR_y
Grouped-register circuit. Open the source or workbench to adapt notation.
Lean rootQuantumBlockEncoding.StatePreparationBenchmarks.mottonenDenseVerified_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(5/13))} & \ctrl{1} & \qw & \ctrl{1} & \qw \\
\lstick{$q_0:\ket0$} & \qw & \gate{R_y} & \targ{} & \gate{R_y} & \targ{}
\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{dense}}\rangle=\frac{39|00\rangle+52|01\rangle+60|10\rangle+144|11\rangle}{169}.
\]

% Dense UCRY tree
\begin{quantikz}[row sep=.4cm,column sep=.45cm]
\lstick{$q_1:\ket0$} & \gate{R_y(2\arccos(5/13))} & \ctrl{1} & \qw & \ctrl{1} & \qw \\
\lstick{$q_0:\ket0$} & \qw & \gate{R_y} & \targ{} & \gate{R_y} & \targ{}
\end{quantikz}
    English proof LaTeX 
    \paragraph{Proof.}
The target is an exact nested-Pythagorean instance: the root split uses 5/13 and 12/13, while the two conditional branches use 3/5,4/5 and 5/13,12/13. Lean proves target normalization, a full unitary completion, the exact typed root-RY plus one-control-UCRY state action, and circuit-derived cost (5,4,0,0).
\begin{enumerate}
  \item The same typed five-gate circuit supplies exact state action and parallel depth four.
\end{enumerate}
Each advertised certificate is the named Lean declaration linked on this page.
    Lean declaration retrieval block 
    import QuantumBlockEncoding

#check QuantumBlockEncoding.StatePreparationBenchmarks.mottonenDenseTarget_normalized
#check QuantumBlockEncoding.StatePreparationBenchmarks.mottonenDenseMatrix_unitary
#check QuantumBlockEncoding.StatePreparationBenchmarks.mottonenDensePrimitive_prepares_target
#check QuantumBlockEncoding.StatePreparationBenchmarks.mottonenDenseVerified_cost
    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 tierpassed4 named root(s)

    Numerically mirrors the exact 5/13,12/13 and 3/5,4/5 Lean angles.

    Current runnable artifact
    executable-exports/SP-PAPERS-001/qiskit/export.py
    Command
    python3 executable-exports/SP-PAPERS-001/qiskit/export.py --case mottonen
    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
    Möttönen et al., Eq. (6)–(8) and Fig. 3, arXiv:quant-ph/0407010
    Contributor
    ASPBE authors
    Current boundary
    Only this exact two-qubit instantiation is closed. General n-qubit state-to-state synthesis, phase synthesis, and paper-wide gate-count formulas remain in Papers.
    Load in task builderContribute a variant