Papers · State Preparation · Resource lemma formalized
Guang Hao Low, Vadym Kliuchnikov, Luke Schaeffer · 2018. 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. (2) Eq. (5) Table 2 Fig. 1(c,d)
What these source locations say. Eq. (2) states the arbitrary target-state problem; Eq. (5) gives the coherent data-lookup interface; Table 2 and Fig. 1(c,d) expose the SelectSwap T-count/space tradeoff used by the finite arithmetic witness.
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.
These declarations are the proof authority for the finite theorem or resource lemma described above.
Paper reproduction boundary
Approximate Clifford+T state preparation, coherent lookup/SelectSwap semantics, dirty-qubit correctness, error accounting, and the full asymptotic optimality 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.