Source anchors. Methods Eqs. (10)-(22), Appendix A.1-A.8, Pinned author Lean divsteps and DQI
Formalized now. Priority source intake; author Lean proofs exist, but no new local4.33.0 certificate is claimed.
Remaining paper-wide scope. Upstream proof audit and4.33.0 adaptation, circuit-to-oracle/register/phase/cleanup bridges, statistical and instance arithmetic, actual resources and independent source/reader gates.
Open source paper ↗ Read formalization plan (not a certificate) Source paper ↗
Source anchors. Theorem 1, Corollary 1, Table I, Appendix B: B14–B19, B28
Formalized now. Not yet reproduced in Lean. The shared finite-matrix substrate is not a Walsh Series Loader certificate.
Remaining paper-wide scope. Walsh ordering and parity semantics, controlled zero-order phase, literal branch identity, normalized error, RUS/amplification and full cost. See StatePreparationWiki spw-walsh and technical card tl-walsh-diagonal-phase. Audit the companion comment 2502.05193v1.
Open source paper ↗ Read formalization plan (not a certificate) Source paper ↗
Source anchors. Theorems II.1, III.1–III.2, IV.1, V.1, VIII.1, Eqs. (15)–(16), (19)–(21), Tables I–II, Fig. 4 signal-sector convention unresolved
Formalized now. Not yet reproduced in Lean. The local fixed cubic diagonal example is only a candidate semantic substrate.
Remaining paper-wide scope. Literal source theorem/circuit mapping, parallel scheduling and cleanup, operator approximation, success/normalized-state error and finite-bit cost. See spw-diagonal and technical card tl-diagonal-postselection; reuse the existing Block Encoding API.
Open source paper ↗ Read formalization plan (not a certificate) Source paper ↗
Source anchors. Eq. (6), Eq. (7), Eq. (8), Fig. 3
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).
Remaining paper-wide scope. 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.
Read reproduction Source paper ↗
Source anchors. Eq. (1), Eq. (3), Eq. (5), Eq. (6)
Formalized now. An exact two-bit product distribution, a typed generic binary-tree circuit and typed factorized circuit preparing the same target, and a Lean-certified resource improvement from (5,4,0,0) to (2,1,0,0).
Remaining paper-wide scope. The general efficiently-integrable recursive probability-loading theorem and an end-to-end arithmetic/integration oracle compiler.
Read reproduction Source paper ↗
Source anchors. Eq. (1), Eq. (2), Theorem 1
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).
Remaining paper-wide scope. The asymptotic sparse synthesis constructions, ancilla/circuit-size tradeoffs, and the matching lower bounds of Theorem 1.
Read reproduction Source paper ↗
Source anchors. Eq. (2), Eq. (5), Table 2, Fig. 1(c,d)
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.
Remaining paper-wide scope. Approximate Clifford+T state preparation, coherent lookup/SelectSwap semantics, dirty-qubit correctness, error accounting, and the full asymptotic optimality theorem.
Read reproduction Source paper ↗
Source anchors. Source anchors queued with reproduction
Formalized now. Not yet reproduced in Lean.
Remaining paper-wide scope. The ancilla-sensitive state-preparation construction, depth/size upper bounds, and the matching optimal-depth statements across the claimed parameter regimes.
Open source paper ↗ Source paper ↗
Source anchors. Source anchors queued with reproduction
Formalized now. Not yet reproduced in Lean.
Remaining paper-wide scope. Universal state-preparation decomposition and its CNOT/depth counts, including the four-qubit benchmark.
Open source paper ↗ Source paper ↗
Source anchors. Source anchors queued with reproduction
Formalized now. The local uniformly-controlled-RY compiler provides a related reusable primitive, but this paper is not claimed reproduced.
Remaining paper-wide scope. Paper-faithful quantum-multiplexor/state-initialization synthesis, its CNOT complexity theorem, and the lower-bound comparison.
Open source paper ↗ Source paper ↗