Appendix D: binary encoding uses exponentially fewer address qubits

Open

QAlgorithms.Papers.Independent.Intakethird100.P67.binary_reencoding

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

prove2quantum

Fix a normalized pure sample family, anchor, history of length $T$ , and $q$ with $2^q\ge T+1$ . Initialize the binary address at zero. The Appendix-D product of coherent anchor tests with cyclic increments and address-selective reflections is exactly the unary erasure state with each unary $|t\rangle$ replaced by binary $|t\rangle$ :

V_{\rm binary}(|\psi\rangle|0\rangle)=\operatorname{Encode}_{q,T}\!\left[|\phi_a\rangle\sum_{t<T}\langle\phi_a|\psi_t\rangle|t\rangle+|\psi_T\rangle|T\rangle\right],\qquad\lceil\log_2(T+1)\rceil\le q.

The ideal main-system output is therefore unchanged. There are absolute constants and a sample-only circuit family, fixed before unknown samples, $U$ and the new input, using $(4T+1)m+1$ supplied copies and at most $C(4T+1)mn(q+1)$ elementary gates on $n$ -qubit systems. Its averaged distance from the same ideal emulator is at most $c(4T+1)/m$ . Apart from supplied-copy registers and the main register, at most $q+3$ helper/address/measurement wires suffice. Thus the reflection sample/error bounds are preserved while the gate overhead is $O(q+1)$ . The constant helper wires are excluded from the advertised address count.

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.22–23, Appendix D: exact binary/unary erasure equality, same ideal
main output, and source sample/gate costs for its sample-copy implementation. The q address
qubits exclude the constant helper/measurement qubits. D8's initial |t> is replaced by |0>;
D9's tensor grouping and |0> helper are corrected to Fig.6's returned |minus>.
Using q+1 (equivalently log(T+1) away from T=0) handles the small-T boundary. -/
theorem binary_reencoding :
    (∀ (phi : K → EuclideanSpace ℂ I) (a : K), (∀ k, IsState (phi k)) →
      ∀ (q T : ℕ), T+1 ≤ 2^q → ∀ (h : Fin T → K) (psi : EuclideanSpace ℂ I), IsState psi →
        act (binaryHistory phi a q h) (tensorVec psi (ket (0 : Fin (2^q)))) =
          encodeUnary q T (coordinateExpansion phi a h psi) ∧
        Nat.clog 2 (T+1) ≤ q) ∧
    (∃ (C c : ℝ) (B : BinaryEmulatorFamily), 0 < C ∧ 0 < c ∧
      ∀ (n k : ℕ), 2 ≤ k → ∀ (a : Fin k) (q T m : ℕ),
        T+1 ≤ 2^q → 1 ≤ m →
        (∀ h : Fin T → Fin k,
          (B n k a q T m h).copies = (4*T+1)*m+1 ∧
          (B n k a q T m h).N ≤ ((4*T+1)*m+2)*n + q+3 ∧
          ((B n k a q T m h).gates.length : ℝ) ≤ C * (4*T+1) * m * n * (q+1)) ∧
        ∀ (phi : Fin k → EuclideanSpace ℂ (Qubits n)), (∀ j, IsState (phi j)) →
          ∀ (U : Matrix.unitaryGroup (Qubits n) ℂ) (rho : Matrix (Qubits n) (Qubits n) ℂ), IsDensityMatrix rho →
          traceDistance
            (∑ h : Fin T → Fin k, (historyWeight (nonanchorProbability a) h : ℂ) •
              (B n k a q T m h).output (inputOutputRecords phi (U : Matrix (Qubits n) (Qubits n) ℂ)) rho)
            (emulate phi a (U : Matrix (Qubits n) (Qubits n) ℂ) T rho) ≤ c * (4*T+1) / m) := by sorry

end QAlgorithms.Papers.Independent.Intakethird100.P67

end

Source

Universal Quantum Emulator, arXiv:1606.02734v2, PDF p. 22, Appendix D: binary encoding uses exponentially fewer address qubits

Read-back

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

Let $I,K$ be finite index types with decidable equality. The declaration asserts a conjunction of two claims. First, for every family of norm-one vectors $\phi_k\in\mathbb C^I$ , every $a\in K$ , every natural $q,T$ satisfying $T+1\le2^q$ , every history $h:\{0,\ldots,T-1\}\to K$ , and every norm-one $\psi\in\mathbb C^I$ , define $E_k=\phi_k\phi_k^\dagger$ , $R_k=1-2E_k$ , $r_0=\psi$ , and $r_{t+1}=R_{h(t)}(1-E_a)r_t$ . Let $u_t\in\{0,1\}^T$ have bit $j$ true exactly when $j<t$ , and set

v=\sum_{t=0}^{T-1}\langle\phi_a,r_t\rangle\,\phi_a\otimes|u_t\rangle +r_T\otimes|u_T\rangle.

For a vector $v$ on $I\times\{0,1\}^T$ , its binary encoding is the vector on $I\times\{0,\ldots,2^q-1\}$ whose $(i,s)$ -coordinate is $\sum_{t=0}^{T}\mathbf1_{s=t}v(i,u_t)$ . Let $J_q|s\rangle=|(s+1)\bmod2^q\rangle$ , let $M=E_a\otimes1+(1-E_a)\otimes J_q$ , and let $A_{j+1}$ apply $R_{h(j)}$ to the system exactly when the address equals $j+1$ , otherwise applying the identity. Then

(A_T M)\cdots(A_1 M)(\psi\otimes|0\rangle) =\operatorname{encode}(v), \qquad \lceil\log_2(T+1)\rceil\le q.

For $T=0$ , the product is the identity and the encoding contains only $r_0=\psi$ ; $q=0$ is permitted and forces $T=0$ . Second, there exist positive real constants $C,c$ and a family $B(n,k,a,q,T,m,h)$ of sample circuits such that, for all natural $n,k$ with $k\ge2$ , all anchors $a$ , and all natural $q,T,m$ with $T+1\le2^q$ and $m\ge1$ , every history $h$ satisfies

\begin{aligned} \operatorname{copies}(B(n,k,a,q,T,m,h))&=(4T+1)m+1,\\ N(B(n,k,a,q,T,m,h))&\le((4T+1)m+2)n+q+3,\\ \operatorname{length}(\operatorname{gates}(B(n,k,a,q,T,m,h))) &\le C(4T+1)mn(q+1). \end{aligned}

Here a sample circuit has injectively placed $n$ -qubit input and sample registers, Boolean-and-sample-index labels for its copies, fixed computational-basis states on other wires, and gates consisting of arbitrary one-qubit unitaries and swaps controlled by two distinct control wires; its output retains the original input ports and traces out the other wires. For every collection of norm-one $\phi_j\in\mathbb C^{\{0,1\}^n}$ , every unitary $U$ , and every positive semidefinite trace-one $\rho$ , initialize sample label $({\rm false},j)$ in $E_j=\phi_j\phi_j^\dagger$ and label $({\rm true},j)$ in $UE_jU^\dagger$ , and call the resulting circuit output $\mathcal O_h(\rho)$ . To specify the comparison matrix, put $p_a=0$ , $p_j=(k-1)^{-1}$ for $j\ne a$ , $\omega_T=|-\rangle\langle-|^{\otimes T}$ , and $W_j=C(1-2E_j)(1\otimes H_{\rm Had})C(1-2E_a)$ , where $C$ is controlled by a true Boolean ancilla and $H_{\rm Had}=2^{-1/2}\begin{pmatrix}1&1\\1&-1\end{pmatrix}$ . Let $V_h$ apply these $W_{h(t)}$ in increasing order on separate ancillas, let $\widetilde V_h$ use $(U\otimes1)W_{h(t)}(U^\dagger\otimes1)$ instead, and put $P_{\rm false}=E_a$ , $P_{\rm true}=1-E_a$ . Define

\mathcal E_T(\rho)= \sum_h\Bigl(\prod_tp_{h(t)}\Bigr) \sum_{b\in\mathrm{Bool}} \operatorname{tr}_{\rm anc}\!\left[ \widetilde V_h^\dagger \left((U\phi_a)(U\phi_a)^\dagger\otimes \operatorname{tr}_{\rm sys}\!\left[ (P_b\otimes1)V_h(\rho\otimes\omega_T)V_h^\dagger(P_b\otimes1) \right]\right)\widetilde V_h\right].

Then, writing $D(X,Y)=\frac12\operatorname{Re}\operatorname{tr}\sqrt{(X-Y)^\dagger(X-Y)}$ , with the square root given by continuous functional calculus, the asserted error bound is

D\!\left(\sum_h\Bigl(\prod_tp_{h(t)}\Bigr)\mathcal O_h(\rho), \mathcal E_T(\rho)\right) \le \frac{c(4T+1)}m.

This second claim includes $n=0$ and $T=0$ , and assumes neither a generation condition on the samples nor a support condition on $\rho$ .

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