Papers · State Preparation · Finite benchmark formalized
Mikko Möttönen, Juha J. Vartiainen, Ville Bergholm, Martti M. Salomaa · 2005. This is a source-facing partial reproduction page: it separates the paper statement, the finite Lean surface already closed in ASPBE, and the paper-wide work still queued.
Source contract
Source anchors. Eq. (6) Eq. (7) Eq. (8) Fig. 3
What these source locations say. Eq. (6) eliminates one qubit by a uniformly controlled y rotation; Eq. (7) composes those eliminations recursively; Eq. (8) specifies the required angles; Fig. 3 displays the resulting state-preparation architecture.
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).
These declarations are the proof authority for the finite theorem or resource lemma described above.
QuantumBlockEncoding.StatePreparationBenchmarks.mottonenDenseTarget_normalizedQuantumBlockEncoding.StatePreparationBenchmarks.mottonenDenseMatrix_unitaryQuantumBlockEncoding.StatePreparationBenchmarks.mottonenDensePrimitive_prepares_targetQuantumBlockEncoding.StatePreparationBenchmarks.mottonenDenseVerified_costPaper reproduction boundary
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.
Status rule. A finite witness, typed circuit, or resource lemma is not silently promoted to the source paper's arbitrary-width or asymptotic theorem.