Papers · State Preparation · Finite sparse benchmark formalized
Lvzhou Li, Jingquan Luo · 2025. 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. (1) Eq. (2) Theorem 1
What these source locations say. Eq. (1) records a d-sparse state through its nonzero amplitudes and basis labels; Eq. (2) is the exact state-preparation unitary contract with clean ancillas; Theorem 1 is the asymptotic circuit-size statement that remains outside the finite ASPBE witness.
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).
These declarations are the proof authority for the finite theorem or resource lemma described above.
QuantumBlockEncoding.StatePreparationBenchmarks.sparseThreeTarget_normalizedQuantumBlockEncoding.StatePreparationBenchmarks.sparseThreeMatrix_unitaryQuantumBlockEncoding.StatePreparationBenchmarks.sparsePruned_prepares_targetQuantumBlockEncoding.StatePreparationBenchmarks.sparseDenseTree_prepares_targetQuantumBlockEncoding.StatePreparationBenchmarks.sparseDenseTreeVerified_costQuantumBlockEncoding.StatePreparationBenchmarks.sparsePrunedVerified_costQuantumBlockEncoding.StatePreparationBenchmarks.sparsePruned_betterThan_denseTreePaper reproduction boundary
The asymptotic sparse synthesis constructions, ancilla/circuit-size tradeoffs, and the matching lower bounds of Theorem 1.
Status rule. A finite witness, typed circuit, or resource lemma is not silently promoted to the source paper's arbitrary-width or asymptotic theorem.