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

State preparation · exact one-qubit circuit

Preparing the equal superposition |+>

Prepare a coherent equal superposition from |0>, including the exact factor 1/sqrt(2).

Lean certifiedA familiar quantum gate becomes a complete exact certificate rather than a numerical statevector check.

Read this before the proof dashboard

See the difference between a classical random bit and a coherent quantum superposition.

Many quantum algorithms need interference. The Hadamard gate is the smallest example where two basis states simultaneously have nonzero amplitudes before measurement.

Preparing |+> is the first step of countless circuits. The important lesson is that amplitudes, not classical probabilities, are transformed coherently by later gates.

Read the circuit

What the wires and stages are doing

1
Start

The wire is |0>, so the amplitude vector is (1,0).

2
Hadamard

H maps the vector to (1/sqrt(2),1/sqrt(2)).

3
Interpret

A computational-basis measurement would return 0 or 1 with equal probability, but before measurement the relative amplitudes can still interfere.

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

Hadamard prepares the equal superposition

\[H|0\rangle=|+\rangle=\frac{|0\rangle+|1\rangle}{\sqrt2},\qquad H^\dagger H=I\]

The exact square-root normalization, unitarity of H, and equality of the zero-input column with |+> are all machine checked.

Proof story

  1. Normalize |+>Each amplitude has squared magnitude 1/2, so the total is 1.
  2. Prove H is unitaryThe two columns are normalized and orthogonal.
  3. Read column zeroMultiplying by |0> selects H's first column, which is the desired amplitude vector.
  4. Record the circuitThe exact preparation uses one H gate and no ancilla.
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

\[H|0\rangle=|+\rangle=\frac{|0\rangle+|1\rangle}{\sqrt 2},\qquad H=\frac1{\sqrt2}\begin{pmatrix}1&1\\1&-1\end{pmatrix}.\]

Lean proves the square-root identity needed for normalization, proves H is complex unitary, and identifies its zero-input column with the target amplitudes.

H
the Hadamard unitary
|+>
the normalized state with equal positive amplitudes

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 Hadamard

H
03

Certified output

system = (|0>+|1>)/sqrt(2)

|+>

Auditable evolution

Candidate and proof progression

One exact candidate is sufficient. The certified score uses the same tuple order as the larger cases.

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.}
\[
H|0\rangle=|+\rangle=\frac{|0\rangle+|1\rangle}{\sqrt 2},\qquad H=\frac1{\sqrt2}\begin{pmatrix}1&1\\1&-1\end{pmatrix}.
\]

% Hadamard candidate
\begin{quantikz}[column sep=.55cm]
\lstick{$\ket0$} & \gate{H} & \rstick{$\ket+ $} \qw
\end{quantikz}
    English proof LaTeX 
    \paragraph{Proof.}
Lean proves the square-root identity needed for normalization, proves H is complex unitary, and identifies its zero-input column with the target amplitudes.
\begin{enumerate}
  \item The candidate closes normalization, unitarity, state action, and cost.
\end{enumerate}
Each advertised certificate is the named Lean declaration linked on this page.
    Lean declaration retrieval block 
    import QuantumBlockEncoding

#check QuantumBlockEncoding.TextbookStatePreparation.hadamard_unitary
#check QuantumBlockEncoding.TextbookStatePreparation.plusTarget_normalized
#check QuantumBlockEncoding.TextbookStatePreparation.hadamardCertificate_prepares_plus
#check QuantumBlockEncoding.TextbookStatePreparation.hadamardVerified_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; numerical statevector output is optional user evidence, not the proof.

    Current runnable artifact
    executable-exports/SP-TEXTBOOK-001/qiskit/export.py
    Command
    python3 executable-exports/SP-TEXTBOOK-001/qiskit/export.py --case hadamard
    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