Prepare |psi> from |0...0>
State Preparation
State-preparation examples and papers: target amplitudes, exact unitary certificates, circuit realizations, and resource-aware improvements.
Reproducible reading paths
Case studies, from equation to circuit
Each case begins with the operator or target state, fixes the acceptance contract, and then shows the circuit and resource trace. “Certified” means a named Lean root compiled in this checkout. Qiskit and other fast backends may screen and prioritize routes; a floating-point match alone is not the final exact proof.
Two reading tracks
Example Cases 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.
How to read a score
The tuple is ordered lexicographically as (gate count, parallel depth, auxiliary qubits, oracle calls). A page says “strictly better” only when it links the corresponding Lean betterThan theorem. Routes at different semantic tiers are not compared.
State preparation
Preparing the basis state |1>
The smallest complete state-preparation certificate: target normalization, unitary matrix, exact state action, and resource tuple.
\[X|0\rangle=|1\rangle,\qquad X=\begin{pmatrix}0&1\\1&0\end{pmatrix}.\]
State preparation
Preparing the equal superposition |+>
A familiar quantum gate becomes a complete exact certificate rather than a numerical statevector check.
\[H|0\rangle=|+\rangle=\frac{|0\rangle+|1\rangle}{\sqrt 2},\qquad H=\frac1{\sqrt2}\begin{pmatrix}1&1\\1&-1\end{pmatrix}.\]
Block encoding
BE Case 1: finite transfer operator
A concrete non-unitary transfer is embedded in a permutation unitary and improved from (6,5,1,0) to (4,2,1,0).
\[E_1=|0\rangle\!\langle1|_{\mathrm{time}}\otimes|0\rangle\!\langle1|_{\mathrm{type}}\otimes I_2,\qquad \langle0|_aU|0\rangle_a=E_1.\]
Block encoding
BE Case 1: isolated cold reconstruction
An isolated route closes the same mathematical contract with its own exact permutation and score (5,5,1,0).
\[E_1=|0\rangle\!\langle1|_{\mathrm{time}}\otimes|0\rangle\!\langle1|_{\mathrm{type}}\otimes I_2,\qquad \langle0|_aU_{\mathrm{cold}}|0\rangle_a=E_1.\]
Block encoding
BE Case 2: cubic diagonal family, cold route
A symbolic exact family theorem replaces finite numerical acceptance with rational Householder certificates for every n.
\[D_n=\operatorname{diag}_{0\le j<2^n}\!\left(\frac{j}{2^n}\right)^3,\qquad \Pi U_n\Pi^\dagger=D_n.\]
Block encoding
BE Case 2: cubic diagonal family, hinted route
A direct hint becomes a short formal route with separate exact Lean roots for the input and output blocks.
\[O_0=\sum_{j=0}^{2^n-1}x_j|j\rangle\!\langle j|,\quad x_j=\frac{j}{2^n},\qquad D_n=O_0^3=\sum_jx_j^3|j\rangle\!\langle j|.\]
Block encoding
GHL Eq. (9) benchmark at N=8 (A1=B1=0)
Lean block-encodes the dimensionless A1=B1=0 specialization of GHL Eq. (9), explicitly distinguishes it from the physical Delta x^{-2} matrix, closes both source realizations and the evolved candidate at the exact primitive level, and certifies the candidate's same-tier improvement.
\[A_{\mathrm{GHL}}^{(9)}=\Delta x^{-2}\,\widetilde A(A_1\Delta x,B_1\Delta x),\qquad \widetilde A_0:=\widetilde A(0,0)=\frac1{12}\begin{pmatrix}-30&32&-2&0&0&0&0&0\\16&-31&16&-1&0&0&0&0\\-1&16&-30&16&-1&0&0&0\\0&-1&16&-30&16&-1&0&0\\0&0&-1&16&-30&16&-1&0\\0&0&0&-1&16&-30&16&-1\\0&0&0&0&-1&16&-31&16\\0&0&0&0&0&-2&32&-30\end{pmatrix},\qquad \Pi U\Pi^\dagger=\frac{\widetilde A_0}{56/3}=\frac{M}{224},\quad M=12\widetilde A_0.\]
State preparation
Bell-state preparation: the first entangled target
The smallest proof-bearing state-preparation case with entanglement: the same typed circuit carries exact semantics and resource accounting.
\[U_{\mathrm{Bell}}|00\rangle=|\Phi^+\rangle=\frac{|00\rangle+|11\rangle}{\sqrt2}.\]
State preparation
Dense real-amplitude preparation: a Möttönen-style two-qubit benchmark
A non-product dense state links the first-column contract to Möttönen's UCRY recursion using an exact proof-bearing primitive circuit.
\[|\psi_{\mathrm{dense}}\rangle=\frac{39|00\rangle+52|01\rangle+60|10\rangle+144|11\rangle}{169}.\]
State preparation
Structured probability loading: product structure beats the generic tree
A structured probability-loading example shows how ASPBE can preserve the exact state while removing conditional structure and reducing certified resources.
\[|\psi_{\mathrm{prod}}\rangle=\left(\frac35|0\rangle+\frac45|1\rangle\right)\otimes\left(\frac35|0\rangle+\frac45|1\rangle\right)=\frac{9|00\rangle+12|01\rangle+12|10\rangle+16|11\rangle}{25}.\]
State preparation
Sparse state preparation: prune the zero branches
A finite Li–Luo Eq. (2) witness isolates the mechanism behind sparse preparation: remove a provably identity zero-amplitude subtree while preserving exact state semantics.
\[|\psi_{\mathrm{sparse}}\rangle=\frac{3|000\rangle+4|010\rangle+12|100\rangle}{13},\qquad d=3.\]
State preparation
Hermite-smoothed initial states
Prepare Hermite samples with a small reusable bond register instead of listing 2^n_p amplitudes: a proved O(n_p (k+1)^3) ideal-gate construction, alongside the retained rotation-tree reference and separately scoped finite exports.
\[\lvert g_k\rangle_p=\frac{1}{\sqrt{Z_k}}\sum_{j=0}^{2^n-1}g_k(p_j)\lvert j\rangle,\quad Z_k=\sum_jg_k(p_j)^2,\quad p_j=-\pi L+\frac{2\pi Lj}{2^n}.\]
Contribute a checked variant
Generated drafts are welcome. Public retrieval begins only after review, a repository declaration, and the advertised gates pass.