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

State preparation · exact finite matrix certificate + exact typed primitive circuit

Bell-state preparation: the first entangled target

Starting from |00>, prepare the Bell state (|00>+|11>)/sqrt(2), so the case introduces entanglement rather than another one-qubit amplitude change.

Lean certifiedThe smallest proof-bearing state-preparation case with entanglement: the same typed circuit carries exact semantics and resource accounting.

Source paper · paper-grounded pedagogical specialization

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. (1) + Sec. III

Eq. (1) Sec. III

What the paper says. Eq. (1) fixes the general n-qubit state-vector convention, while Sec. III states the state-preparation problem as finding U with U|a> = |b>.

What ASPBE does here. ASPBE specializes that general contract to the Bell target (|00>+|11>)/sqrt(2). The H-then-CX witness is a textbook teaching circuit; we do not claim that this two-gate Bell example is copied from Möttönen et al.

Open source paper ↗

Read this before the proof dashboard

Understand entanglement as an exact state-preparation contract carried by a concrete two-gate unitary circuit.

The Bell target cannot be represented as two independently prepared one-qubit states. The proof-bearing route creates one coherent branch bit and then correlates the second wire with it.

Small entangled resource states occur throughout teleportation, communication, phase-estimation subroutines, and error-correcting constructions.

Read the circuit

What the wires and stages are doing

1
Start

Both qubits begin in |0>.

2
Superpose q0

RY(pi/2) produces equal positive |0> and |1> amplitudes.

3
Entangle

CX maps the |01> branch to |11>.

4
Check the object actually scored

The same typed two-gate circuit is evaluated in Lean and supplies the resource tuple.

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 typed Bell circuit prepares the exact Bell state

\[U_{\mathrm{Bell}}|00\rangle=(|00\rangle+|11\rangle)/\sqrt2\]

Lean checks target normalization, full unitary completion, exact primitive-circuit state action, and the two-gate/two-layer cost.

Proof story

  1. NormalizeTwo amplitudes have squared magnitude 1/2.
  2. Fix RY conventionReuse the exact standard RY(pi/2) matrix theorem.
  3. Apply CXThe basis permutation sends the q0=1 branch to |11>.
  4. ComposeChronological circuit evaluation proves the two stages prepare the target.
  5. Count the same circuitThe typed circuit itself yields cost (2,2,0,0).
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

\[U_{\mathrm{Bell}}|00\rangle=|\Phi^+\rangle=\frac{|00\rangle+|11\rangle}{\sqrt2}.\]

Lean proves normalization, a full 4 by 4 unitary completion, and an exact typed primitive route RY(pi/2) followed by CX whose zero-input action is the Bell state. The resource tuple (2,2,0,0) is computed from that same circuit. H followed by CX is an equivalent textbook witness, not the proof-bearing circuit scored here.

|Phi+>
the maximally entangled Bell state
RY(pi/2)
the exact primitive rotation that creates equal positive amplitudes on q0
CX
controlled-X that maps the |01> branch to |11>

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

Create superposition

RY(pi/2) on q0 produces equal positive amplitudes

RY(pi/2, q0)
02

Entangle

CX(q0,q1) maps the excited q0 branch to |11>

CX(q0,q1)

Auditable evolution

Candidate and proof progression

This is a proof trace, not a search claim: the scored two-gate circuit is itself the object whose exact state action Lean proves.

iteration0

Bell RY+CNOT

Lean certified

The typed primitive circuit prepares the exact Bell target and supplies its own resource tuple.

Bell RY+CNOTq_0:ket0R_y(pi/2)q_1:ket0|Phi^+rangle
Grouped-register circuit. Open the source or workbench to adapt notation.
Lean rootQuantumBlockEncoding.StatePreparationBenchmarks.bellVerified_cost Edit and preview this stage →
Copy this stage as quantikz 
\begin{quantikz}[row sep=.4cm,column sep=.55cm]
\lstick{$q_0:\ket0$} & \gate{R_y(\pi/2)} & \ctrl{1} & \qw \\
\lstick{$q_1:\ket0$} & \qw & \targ{} & \rstick{$|\Phi^+\rangle$} \qw
\end{quantikz}
2gates2depth0aux0oracles

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.}
\[
U_{\mathrm{Bell}}|00\rangle=|\Phi^+\rangle=\frac{|00\rangle+|11\rangle}{\sqrt2}.
\]

% Bell RY+CNOT
\begin{quantikz}[row sep=.4cm,column sep=.55cm]
\lstick{$q_0:\ket0$} & \gate{R_y(\pi/2)} & \ctrl{1} & \qw \\
\lstick{$q_1:\ket0$} & \qw & \targ{} & \rstick{$|\Phi^+\rangle$} \qw
\end{quantikz}
    English proof LaTeX 
    \paragraph{Proof.}
Lean proves normalization, a full 4 by 4 unitary completion, and an exact typed primitive route RY(pi/2) followed by CX whose zero-input action is the Bell state. The resource tuple (2,2,0,0) is computed from that same circuit. H followed by CX is an equivalent textbook witness, not the proof-bearing circuit scored here.
\begin{enumerate}
  \item The typed primitive circuit prepares the exact Bell target and supplies its own resource tuple.
\end{enumerate}
Each advertised certificate is the named Lean declaration linked on this page.
    Lean declaration retrieval block 
    import QuantumBlockEncoding

#check QuantumBlockEncoding.StatePreparationBenchmarks.bellTarget_normalized
#check QuantumBlockEncoding.StatePreparationBenchmarks.bellMatrix_unitary
#check QuantumBlockEncoding.StatePreparationBenchmarks.bellPrimitive_prepares_target
#check QuantumBlockEncoding.StatePreparationBenchmarks.bellVerified_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 RY(pi/2)+CX Lean route; Qiskit is inspection evidence, not proof authority.

    Current runnable artifact
    executable-exports/SP-PAPERS-001/qiskit/export.py
    Command
    python3 executable-exports/SP-PAPERS-001/qiskit/export.py --case bell
    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. (1) + Sec. III as the general state-preparation contract; Bell is an ASPBE pedagogical specialization
    Contributor
    ASPBE authors
    Current boundary
    Fixed two-qubit target. This is a pedagogical specialization, not a claim that Möttönen et al. present this Bell circuit.
    Load in task builderContribute a variant