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

State preparation · exact one-qubit circuit

Preparing the basis state |1>

Starting from the computational-basis zero state, construct a one-qubit unitary whose output is exactly |1>.

Lean certifiedThe smallest complete state-preparation certificate: target normalization, unitary matrix, exact state action, and resource tuple.

Read this before the proof dashboard

Learn what state preparation means before seeing a complicated data-loading circuit.

A quantum algorithm must begin in a quantum state. This one-qubit example isolates that input-access problem: can a circuit take the easy state |0> to the requested target |1>?

This is not claiming a speedup. It is the smallest possible instance of the same contract used when a larger algorithm asks for an input state |psi>.

Read the circuit

What the wires and stages are doing

1
Start

The wire begins in |0>.

2
Gate

The X box swaps the amplitudes of |0> and |1>.

3
Finish

The output is exactly |1>; there is no ancilla and no measurement in the certificate.

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

Pauli X prepares the basis state |1>

\[X|0\rangle=|1\rangle,\qquad X^\dagger X=I\]

The target vector is normalized, X is unitary, and applying X to the zero basis state returns the target exactly.

Proof story

  1. Normalize the targetThe target has one amplitude equal to 1 and all others 0, so its norm is 1.
  2. Prove unitarityX is a permutation matrix and therefore preserves the computational basis and inner products.
  3. Check the zero inputThe first column of X is exactly the vector |1>.
  4. Package the certificateThe target, circuit, semantic proof, and one-gate resource record are stored together.
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

\[X|0\rangle=|1\rangle,\qquad X=\begin{pmatrix}0&1\\1&0\end{pmatrix}.\]

Lean proves normalization of the target, unitarity of X, and the exact matrix-vector equation. No sampled amplitudes or floating-point tolerance enters the certificate.

|0>, |1>
the two computational-basis states
X
the Pauli X unitary, which exchanges the two basis states

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

Input

system = |0>

|0>
02

Unitary

apply Pauli X

X
03

Certified output

system = |1>

|1>

Auditable evolution

Candidate and proof progression

This textbook case closes in one candidate; the plot is a proof-and-resource trace, not a search claim.

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.}
\[
X|0\rangle=|1\rangle,\qquad X=\begin{pmatrix}0&1\\1&0\end{pmatrix}.
\]

% X candidate
\begin{quantikz}[column sep=.55cm]
\lstick{$\ket0$} & \gate{X} & \rstick{$\ket1$} \qw
\end{quantikz}
    English proof LaTeX 
    \paragraph{Proof.}
Lean proves normalization of the target, unitarity of X, and the exact matrix-vector equation. No sampled amplitudes or floating-point tolerance enters the certificate.
\begin{enumerate}
  \item The first and only candidate satisfies the exact state-action contract.
\end{enumerate}
Each advertised certificate is the named Lean declaration linked on this page.
    Lean declaration retrieval block 
    import QuantumBlockEncoding

#check QuantumBlockEncoding.TextbookStatePreparation.pauliX_unitary
#check QuantumBlockEncoding.TextbookStatePreparation.oneTarget_normalized
#check QuantumBlockEncoding.TextbookStatePreparation.pauliXCertificate_prepares_one
#check QuantumBlockEncoding.TextbookStatePreparation.pauliXVerified_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 OperatorGate-by-gate numerical screeningartifact availableexecutable-exports/SP-TEXTBOOK-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)

    Exports the certified gate as runnable Qiskit code; it is not used to decide the theorem.

    Current runnable artifact
    executable-exports/SP-TEXTBOOK-001/qiskit/export.py
    Command
    python3 executable-exports/SP-TEXTBOOK-001/qiskit/export.py --case pauli-x
    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 textbook example
    Contributor
    ASPBE authors
    Current boundary
    One qubit; no synthesis search is needed.
    Load in task builderContribute a variant