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.
Queued
Discovering state-of-the-art quantum circuits with large language models
Andi Gu, Alek H. Kemeny, Susanne F. Yelin, Mikhail D. Lukin · 2026
Formalized now. Priority source intake; author Lean proofs exist, but no new local4.33.0 certificate is claimed.
Still required for paper reproduction. Upstream proof audit and4.33.0 adaptation, circuit-to-oracle/register/phase/cleanup bridges, statistical and instance arithmetic, actual resources and independent source/reader gates.
Queued
Efficient Quantum State Preparation with Walsh Series
Julien Zylberman, Fabrice Debbasch · 2024
Formalized now. Not yet reproduced in Lean. The shared finite-matrix substrate is not a Walsh Series Loader certificate.
Still required for paper reproduction. Walsh ordering and parity semantics, controlled zero-order phase, literal branch identity, normalized error, RUS/amplification and full cost. See StatePreparationWiki spw-walsh and technical card tl-walsh-diagonal-phase. Audit the companion comment 2502.05193v1.
Queued
Efficient Quantum Circuits for Non-Unitary and Unitary Diagonal Operators with Space-Time-Accuracy trade-offs
Julien Zylberman, Ugo Nzongani, Andrea Simonetto, Fabrice Debbasch · 2025
Formalized now. Not yet reproduced in Lean. The local fixed cubic diagonal example is only a candidate semantic substrate.
Still required for paper reproduction. Literal source theorem/circuit mapping, parallel scheduling and cleanup, operator approximation, success/normalized-state error and finite-bit cost. See spw-diagonal and technical card tl-diagonal-postselection; reuse the existing Block Encoding API.
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.