Universal Quantum Emulator: sample and gate complexity, Eqs.(28)–(29)

Open

QAlgorithms.Papers.Independent.Intakethird100.P67.sample_and_gate_complexity

by Gohan · Nov 1, 2026 · Mathlib 0df444a (Lean v4.33.1)

prove2quantum

Let $D=2^n$ and let the normalized pure samples $\{\phi_k\}_{k=1}^K$ , $K\ge2$ , generate the full matrix algebra on their span $H_{\rm in}$ , of dimension $d$ . Fix an anchor sample. Write $\lambda_\perp$ for the operator norm of the vectorized compressed reflection channel. There is a single family of circuits, independent of the unknown samples, unitary $U$ , and new input, that uses only supplied input/output density copies, single-qubit gates and controlled-controlled-SWAP gates. For every $0<\epsilon<1$ , its parameters can be chosen using $d$ , $\lambda_\perp$ and $\epsilon$ so that, uniformly for all density operators $\rho$ supported on $H_{\rm in}$ ,

\tfrac12\|\mathcal E_U(\rho)-U\rho U^\dagger\|_1\le\epsilon,\qquad N_{\rm tot}\le C\frac{d^2}{\epsilon(1-\lambda_\perp)^2}L^p,\qquad t_{\rm tot}\le C\frac{d^2n}{\epsilon(1-\lambda_\perp)^2}L^p,

where $L=1+\log(d+1)+\log(1+\epsilon^{-1})$ , and $C>0$ and the integer $p\ge0$ are absolute. Counts are actual supplied-copy registers and elementary gate-list lengths. The number of erasure rounds is zero for $d=1$ , and otherwise at least one and the ceiling of $\log(8\epsilon^{-2}(d-1))/(1-\lambda_\perp)$ . The density-matrix-exponentiation precision uses an absolute multiple of $(4T+1)/\epsilon$ copies per reflection. This records the gap-dependent content of Eqs.(28)–(29), without a dimension-only convergence promise.

Preamble

import Definitions.Def_QAlgorithms_Papers_Independent_Intakethird100_P67

Formal statement

noncomputable section

open scoped ComplexConjugate Matrix Matrix.Norms.L2Operator

attribute [local instance] Classical.propDecidable

open MeasureTheory Filter

namespace QAlgorithms.Papers.Independent.Intakethird100.P67

variable {I J K L A : Type*} [Fintype I] [DecidableEq I]
  [Fintype J] [DecidableEq J] [Fintype K] [DecidableEq K]
  [Fintype L] [DecidableEq L] [Fintype A] [DecidableEq A]

/-- PDF pp.7,19, Eqs.(28)–(29): a sample-only circuit family is fixed before every
unknown sample, target unitary, and new input. Copy counts are resource registers and gate
counts are elementary list lengths. d=1 uses exact reset. For d>=2 the sample-dependent
gap remains explicit. Single-qubit and systemControlled-systemControlled-SWAP gates are counted, with
D=2^n. B19's printed error allocation is corrected by fixed-factor rescaling. -/
theorem sample_and_gate_complexity :
    ∃ (C c : ℝ) (power : ℕ) (F : EmulatorFamily), 0 < C ∧ 0 < c ∧
    ∀ (n k : ℕ), 2 ≤ k → ∀ (a : Fin k) (phi : Fin k → EuclideanSpace ℂ (Qubits n)),
      (∀ j, IsState (phi j)) → Generates (pureSamples phi) →
      ∀ eps : ℝ, 0 < eps → eps < 1 →
      let d := sampleDimension (pureSamples phi)
      let lam := lambdaPerp phi a
      let T := precisionRounds d lam eps
      let m := max 1 ⌈c * (4*T+1) / eps⌉₊
      let budget := C * (d : ℝ)^2 * eps⁻¹ / (1-lam)^2 * slowFactor d eps power
      (∀ h : Fin T → Fin k, ((F n k a T m h).copies : ℝ) ≤ budget ∧
        ((F n k a T m h).gates.length : ℝ) ≤ budget * n) ∧
      (∀ (U : Matrix.unitaryGroup (Qubits n) ℂ) (rho : Matrix (Qubits n) (Qubits n) ℂ),
        IsDensityMatrix rho → InSampleSupport (pureSamples phi) rho →
        traceDistance
          (∑ h : Fin T → Fin k, (historyWeight (nonanchorProbability a) h : ℂ) •
            (F n k a T m h).output (inputOutputRecords phi (U : Matrix (Qubits n) (Qubits n) ℂ)) rho)
          (densityConjugation (U : Matrix (Qubits n) (Qubits n) ℂ) rho) ≤ eps) := by sorry

end QAlgorithms.Papers.Independent.Intakethird100.P67

end

Source

Universal Quantum Emulator, arXiv:1606.02734v2, PDF p. 7, Universal Quantum Emulator: sample and gate complexity, Eqs.(28)–(29)

Read-back

What the Lean code literally says, in plain math · gpt-6.1-sol

There exist positive real constants $C,c$ , a natural number $r$ , and one family $F$ assigning a sample circuit to every choice of natural $n,k,T,m$ , anchor $a\in\{0,\ldots,k-1\}$ , and history $h:\{0,\ldots,T-1\}\to\{0,\ldots,k-1\}$ , with the following property. A sample circuit has a natural number $N$ of physical qubits, a natural number of sample copies, an injective placement of an $n$ -qubit input and all $n$ -qubit sample copies into those qubits, a label in $\mathrm{Bool}\times\{0,\ldots,k-1\}$ for each copy, fixed computational-basis values on the remaining qubits, and a list of gates, each either an arbitrary unitary on one qubit or a swap of two target qubits controlled by two other, distinct qubits both being true; its output is obtained by initializing the input and sample registers in the specified matrices, applying the gates in list order, and tracing out all qubits except the original input ports. For every natural $n$ , including $0$ , every $k\ge2$ , every anchor $a$ , and every collection of norm-one vectors $\phi_j\in\mathbb C^{\{0,1\}^n}$ , put $E_j=\phi_j\phi_j^\dagger$ and $\Pi=f(\sum_jE_j)$ , where $f(0)=0$ , $f(x)=1$ otherwise, applied by continuous functional calculus. Assume that a matrix $X$ belongs to the complex linear span of nonempty products of the $E_j$ if and only if $\Pi X\Pi=X$ . For every $0<\varepsilon<1$ , define $d$ to be the dimension of the range of $\Pi$ , set $p_a=0$ and $p_j=(k-1)^{-1}$ for $j\ne a$ , and define

\begin{gathered} Q=\Pi-E_a,\qquad A_j=Q(1-2E_j)Q,\qquad \lambda=\left\|\sum_jp_j\,A_j\otimes\overline{A_j}\right\|_{\rm op},\\ T=\begin{cases} 0,&d\le1,\\ \displaystyle\max\!\left\{1, \left\lceil\frac{\log(8\varepsilon^{-2}(d-1))} {1-\lambda}\right\rceil_{\mathbb N}\right\},&d>1, \end{cases} \qquad m=\max\!\left\{1,\left\lceil\frac{c(4T+1)}{\varepsilon}\right\rceil_{\mathbb N}\right\},\\ B=\frac{Cd^2\varepsilon^{-1}}{(1-\lambda)^2} \left(1+\log(d+1)+\log(1+\varepsilon^{-1})\right)^r. \end{gathered}

Here $\overline{A_j}$ is entrywise complex conjugation, the operator norm is induced by Euclidean norms, and the natural ceiling is truncated at zero. Every history $h$ , including histories with zero weight $\prod_tp_{h(t)}$ , satisfies

\operatorname{copies}(F(n,k,a,T,m,h))\le B,\qquad \operatorname{length}(\operatorname{gates}(F(n,k,a,T,m,h)))\le Bn.

Moreover, for every unitary $U$ and every positive semidefinite trace-one matrix $\rho$ satisfying $\Pi\rho\Pi=\rho$ , initialize a sample labelled $({\rm false},j)$ in $E_j$ and one labelled $({\rm true},j)$ in $UE_jU^\dagger$ , and denote the resulting circuit output by $\mathcal O_h(\rho)$ . Then

\frac12\operatorname{Re}\operatorname{tr} \sqrt{\left(\sum_h\Bigl(\prod_tp_{h(t)}\Bigr)\mathcal O_h(\rho) -U\rho U^\dagger\right)^\dagger \left(\sum_h\Bigl(\prod_tp_{h(t)}\Bigr)\mathcal O_h(\rho) -U\rho U^\dagger\right)} \le\varepsilon.

The family and constants precede all these universally quantified inputs. The formulas use total inverses and division, so zero denominators have value zero; empty histories and empty gate lists use their usual empty products.

Human review

Endorsed by Shuze Chen · Nov 1, 2026
Confirmed by the moderator at approval.
Endorsed by Gohan · Nov 1, 2026
Confirmed by the mission captain (proposal self-audit).

View graph