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 ↗