§III remarks: emulating the inverse with the same samples

Open

QAlgorithms.Papers.Independent.Intakethird100.P67.inverse_emulation

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

prove2quantum

Let $K\ge2$ normalized pure input samples generate the full algebra on their span, and let their output records be the exact images under an unknown unitary $U$ . The output samples also generate the full algebra on their span $H_{\rm out}$ . Running the same emulator with input and output samples exchanged gives, for every $\epsilon>0$ , a threshold $N$ such that all $T\ge N$ and all density operators supported on $H_{\rm out}$ satisfy

\tfrac12\|\mathcal E_{\rm reverse,T}(\rho)-U^\dagger\rho U\|_1\le\epsilon.

The threshold is uniform over the new input. The construction uses the supplied records in reverse roles; it does not query an inverse-unitary oracle.

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 p.4: swapping the supplied records implements U-dagger uniformly on H_out.
The circuit accesses samples, not a callable U-dagger. -/
theorem inverse_emulation (phi : K → EuclideanSpace ℂ I) (a : K)
    (hK : 2 ≤ Fintype.card K) (hphi : ∀ k, IsState (phi k))
    (hgen : Generates (pureSamples phi)) (U : Matrix.unitaryGroup I ℂ) :
    let out := fun k => act (U : Matrix I I ℂ) (phi k)
    Generates (pureSamples out) ∧ ∀ eps : ℝ, 0 < eps → ∃ N : ℕ, ∀ T ≥ N,
      ∀ rho : Matrix I I ℂ, IsDensityMatrix rho → InSampleSupport (pureSamples out) rho →
      traceDistance (emulate out a (U : Matrix I I ℂ)ᴴ T rho) (densityConjugation (U : Matrix I I ℂ)ᴴ rho) ≤ eps := by sorry

end QAlgorithms.Papers.Independent.Intakethird100.P67

end

Source

Universal Quantum Emulator, arXiv:1606.02734v2, PDF p. 4, §III remarks: emulating the inverse with the same samples

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, let $|K|\ge2$ , fix $a\in K$ , and let every $\phi_k\in\mathbb C^I$ have norm $1$ . For any family $v_k$ , write $P_k^v=v_kv_k^\dagger$ and let $\Pi_v$ be the functional-calculus value of $x\mapsto\mathbf1_{x\ne0}$ on $\sum_kP_k^v$ ; say that this family generates its corner when the complex span of all nonempty products of the $P_k^v$ equals $\{X:\Pi_vX\Pi_v=X\}$ . Assume that $\phi$ generates its corner, and let $U$ be unitary. Define $\chi_k=U\phi_k$ . The assertion is that $\chi$ also generates its corner and that the following uniform approximation holds. To specify its map, put $p_a=0$ , $p_k=(|K|-1)^{-1}$ for $k\ne a$ , $C(V)=1_I\otimes|0\rangle\langle0|+V\otimes|1\rangle\langle1|$ , $H=2^{-1/2}\begin{pmatrix}1&1\\1&-1\end{pmatrix}$ , and

E_k=C(1-2P_k^\chi)(1_I\otimes H)C(1-2P_a^\chi).

For $h\in K^T$ , let $V_h$ be the product applying $E_{h_j}$ to system and ancilla $j$ , in increasing application order, let $\widehat V_h$ use $(U^\dagger\otimes1_2)E_{h_j}(U\otimes1_2)$ instead, and put $X_h=V_h(\rho\otimes\eta_T\eta_T^\dagger)V_h^\dagger$ , where $\eta_T=((|0\rangle-|1\rangle)/\sqrt2)^{\otimes T}$ . Set $P_{\mathrm{false}}=P_a^\chi$ , $P_{\mathrm{true}}=1-P_a^\chi$ , and define

\mathcal E_T(\rho)= \operatorname{Tr}_{\mathrm{anc}} \sum_{h\in K^T}\left(\prod_{j<T}p_{h_j}\right) \sum_b\widehat V_h^\dagger \left[ U^\dagger P_a^\chi U\otimes \operatorname{Tr}_{I}\!\left((P_b\otimes1)X_h(P_b\otimes1)\right) \right]\widehat V_h.

Empty history products are identities. For every real $\varepsilon>0$ , there exists a natural number $N$ such that, for every $T\ge N$ and every positive semidefinite matrix $\rho$ of trace $1$ satisfying $\Pi_\chi\rho\Pi_\chi=\rho$ ,

\tfrac12\operatorname{Re}\operatorname{tr} \sqrt{(\mathcal E_T(\rho)-U^\dagger\rho U)^\dagger (\mathcal E_T(\rho)-U^\dagger\rho U)} \le\varepsilon.

In particular, $N$ is chosen before $\rho$ , and no upper bound on $\varepsilon$ is imposed.

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