Prepare |psi> from |0...0>
State Preparation
State-preparation examples and papers: target amplitudes, exact unitary certificates, circuit realizations, and resource-aware improvements.
Source papers · theorem → proof → Lean scope
Papers
Paper reproductions are a first-class reading track, parallel to Chapters and Example Cases. A paper page starts from the source theorem and proof, states the exact formalization boundary, and only then shows the Lean evidence or ASPBE improvement.
Two reading tracks
Papers by quantum interface
Use the same split everywhere: State Preparation asks for a unitary that prepares a target state; Block Encoding asks for a larger unitary whose selected clean block equals a target operator up to normalization.
Embed A/alpha into a unitary block
Block Encoding
Block-encoding examples and papers: clean-block semantics, oracle access, source constructions, and same-target circuit improvements.
Published reproductions
Read source-facing formalizations
Robin/GHL is the first full paper-map surface. More papers move here only when their public source-to-Lean contract is ready.
Reproduced fixed benchmark
Quantum Framework for Simulating Linear PDEs with Robin Boundary Conditions
Nikita Guseynov, Xiajie Huang, Nana Liu · 2025
Theorem 3/4 are mapped to explicit Lean scope. The fixed N=8 Robin benchmark closes source normal forms, an exact XOR four-slot winner, and same-tier resource comparisons; the arbitrary-width primitive compiler remains a separate frontier.
Paper reproduction queue
What has a finite theorem today, and what still needs the paper-wide proof
A fixed benchmark, a resource-formula lemma, and a complete paper reproduction are different statuses. This queue makes that boundary public.
Finite benchmark formalized
Transformation of quantum states using uniformly controlled rotations
Mikko Möttönen, Juha J. Vartiainen, Ville Bergholm, Martti M. Salomaa · 2005
Formalized now. An exact dense two-qubit target, full unitary completion, typed root-RY plus one-control-UCRY circuit, exact clean-input state action, and the circuit-derived resource tuple (5 gates, depth 4, no auxiliary qubits, no unresolved oracle calls).
Still required for paper reproduction. General n-qubit state-to-state synthesis, phase layer, analytic rotation-angle construction at arbitrary width, and the paper-wide CNOT/one-qubit rotation count theorem.
Structured benchmark formalized
Creating superpositions that correspond to efficiently integrable probability distributions
Lov Grover, Terry Rudolph · 2002
Formalized now. An exact two-bit product distribution, a typed generic binary-tree circuit and typed factorized circuit preparing the same target, and a Lean-certified resource improvement from (5,4,0,0) to (2,1,0,0).
Still required for paper reproduction. The general efficiently-integrable recursive probability-loading theorem and an end-to-end arithmetic/integration oracle compiler.
Finite sparse benchmark formalized
Nearly Optimal Circuit Size for Sparse Quantum State Preparation
Lvzhou Li, Jingquan Luo · 2025
Formalized now. An exact n=3, d=3 witness of Eq. (2), a typed pruned UCRY route, a same-target typed dense zero-fill baseline, and a Lean-certified resource improvement from (15,13,0,0) to (5,4,0,0).
Still required for paper reproduction. The asymptotic sparse synthesis constructions, ancilla/circuit-size tradeoffs, and the matching lower bounds of Theorem 1.
Resource lemma formalized
Trading T gates for dirty qubits in state preparation and unitary synthesis
Guang Hao Low, Vadym Kliuchnikov, Luke Schaeffer · 2018
Formalized now. The clean-qubit SelectSwap T-count formula at the repository arithmetic tier, including N=16, b=1 values 72 at lambda=1 and 48 at lambda=4, plus the strict finite comparison 48<72.
Still required for paper reproduction. Approximate Clifford+T state preparation, coherent lookup/SelectSwap semantics, dirty-qubit correctness, error accounting, and the full asymptotic optimality theorem.
Queued
Asymptotically Optimal Circuit Depth for Quantum State Preparation and General Unitary Synthesis
Xiaoming Sun, Guojing Tian, Shuai Yang, Pei Yuan, Shengyu Zhang · 2021
Formalized now. Not yet reproduced in Lean.
Still required for paper reproduction. The ancilla-sensitive state-preparation construction, depth/size upper bounds, and the matching optimal-depth statements across the claimed parameter regimes.
Queued
Quantum-state preparation with universal gate decompositions
Martin Plesch, Časlav Brukner · 2011
Formalized now. Not yet reproduced in Lean.
Still required for paper reproduction. Universal state-preparation decomposition and its CNOT/depth counts, including the four-qubit benchmark.
Queued
Synthesis of Quantum Logic Circuits
Vivek V. Shende, Stephen S. Bullock, Igor L. Markov · 2006
Formalized now. The local uniformly-controlled-RY compiler provides a related reusable primitive, but this paper is not claimed reproduced.
Still required for paper reproduction. Paper-faithful quantum-multiplexor/state-initialization synthesis, its CNOT complexity theorem, and the lower-bound comparison.