exact one-qubit circuit
Preparing the basis state |1>
The smallest complete state-preparation certificate: target normalization, unitary matrix, exact state action, and resource tuple.
Lean certified
Example Cases · State Preparation
State Preparation example cases
State-preparation examples and papers: target amplitudes, exact unitary certificates, circuit realizations, and resource-aware improvements. Paper-derived cases identify the exact source equation, theorem, figure, table, or section before the ASPBE specialization.
Certified examples
Read the contract, source anchor, proof story, circuit, and Lean evidence
exact one-qubit circuit
Preparing the equal superposition |+>
A familiar quantum gate becomes a complete exact certificate rather than a numerical statevector check.
Lean certified
exact finite matrix certificate + exact typed primitive circuit
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.
Lean certified
exact dense target + exact typed root-RY/UCRY circuit
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.
Lean certified
two exact typed circuits + same-target resource theorem
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.
Lean certified
exact d=3 target + two exact typed same-target circuits
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.
Lean certified
Exact Hermite target; polynomial-gate Bernstein–MPS construction; finite export evidence remains separate
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.
Lean certified