Appendix G2, Eq.(G2): bridge samples enable controlled emulation

Open

QAlgorithms.Papers.Independent.Intakethird100.P67.controlled_with_bridge

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

prove2quantum

Let a finite nonempty mixed sample family generate all operators on $H_{\rm in}$ . Take a unit vector $\phi\in H_{\rm in}$ and normalized control amplitudes $\alpha,\beta$ with both nonzero. In addition to tagged original samples, supply the pure bridge $|\Phi_{\rm in}\rangle=|\phi\rangle(\alpha|0\rangle+\beta|1\rangle)$ and its exact output $|\Phi_{\rm out}\rangle=U^c|\Phi_{\rm in}\rangle$ . The augmented input family satisfies

\operatorname{Alg}_{\mathbb C}\!\left(\{\rho_k\otimes|b\rangle\langle b|:b=0,1\}\cup\{|\Phi_{\rm in}\rangle\langle\Phi_{\rm in}|\}\right)=\mathcal L(H_{\rm in}\otimes\mathbb C^2).

The actual mixed-sample emulator with this pure anchor consequently converges uniformly to controlled conjugation on supported input density operators. The bridge output supplies the relative phase; that phase is not inferred from the original density records.

The tagged output resources are $\rho_k^{\rm in}\otimes|0\rangle\langle0|$ and $\rho_k^{\rm out}\otimes|1\rangle\langle1|$ , together with the output bridge; controlled $U$ leaves the zero-control branch unchanged.

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.28, G2: nonzero control amplitudes in an additional pure bridge generate
the full systemControlled-space algebra and enable emulation by the actual mixed-sample channel.
Printed: the final output-record list uses both control projectors tensor S_out.
Changed: the constructed target-conjugated records use S_in on control zero and
S_out on control one, plus the given output bridge. Why: the defined controlled-U
acts as identity on control zero; these records are available from the given resources. -/
theorem controlled_with_bridge [Nonempty K] (S : K → Matrix I I ℂ)
    (hS : ∀ k, IsDensityMatrix (S k)) (hgen : Generates S)
    (phi : EuclideanSpace ℂ I) (hphi : IsState phi)
    (hsupport : InSampleSupport S (pureDensity phi)) (alpha beta : ℂ)
    (hnorm : ‖alpha‖ ^ 2 + ‖beta‖ ^ 2 = 1) (halpha : alpha ≠ 0) (hbeta : beta ≠ 0) :
    let B := bridgeSamples S phi alpha beta
    let bridge := tensorVec phi (WithLp.toLp 2 fun b => if b then beta else alpha)
    Generates B ∧ ∀ (U : Matrix.unitaryGroup I ℂ) (eps : ℝ), 0 < eps →
      ∃ N : ℕ, ∀ T ≥ N, ∀ rho : Matrix (I × Bool) (I × Bool) ℂ, IsDensityMatrix rho → InSampleSupport B rho →
        traceDistance (mixedEmulate B none bridge (systemControlled (U : Matrix I I ℂ)) T rho)
          (densityConjugation (systemControlled (U : Matrix I I ℂ)) rho) ≤ eps := by sorry

end QAlgorithms.Papers.Independent.Intakethird100.P67

end

Source

Universal Quantum Emulator, arXiv:1606.02734v2, PDF p. 28, Appendix G2, Eq.(G2): bridge samples enable controlled emulation

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, with $K$ nonempty. Let every $S_k$ be positive semidefinite of trace $1$ , let $\Pi_S$ be the functional-calculus value of $x\mapsto\mathbf1_{x\ne0}$ on $\sum_kS_k$ , and assume that the complex span of all nonempty products of the $S_k$ equals $\{X:\Pi_SX\Pi_S=X\}$ . Let $\phi\in\mathbb C^I$ have norm $1$ and satisfy $\Pi_S\phi\phi^\dagger\Pi_S=\phi\phi^\dagger$ , and let $\alpha,\beta\in\mathbb C$ satisfy $|\alpha|^2+|\beta|^2=1$ , $\alpha\ne0$ , and $\beta\ne0$ . On $\mathcal H=\mathbb C^I\otimes\mathbb C^2$ , put $\xi=\phi\otimes(\alpha|0\rangle+\beta|1\rangle)$ , and define the family indexed by $\Lambda=\{\mathrm{none}\}\sqcup(\{\mathrm{false},\mathrm{true}\}\times K)$ by

B_{\mathrm{none}}=\xi\xi^\dagger, \qquad B_{(b,k)}=S_k\otimes|b\rangle\langle b|.

Let $\Pi_B$ be the functional-calculus value of $x\mapsto\mathbf1_{x\ne0}$ on $\sum_{\ell\in\Lambda}B_\ell$ . The assertion is that the complex span of all nonempty products of the $B_\ell$ equals $\{X:\Pi_BX\Pi_B=X\}$ , and that the following approximation holds. For a unitary $U$ on $\mathbb C^I$ , put $Z=1_I\otimes|0\rangle\langle0|+U\otimes|1\rangle\langle1|$ . For operators on $\mathcal H$ , define $C_{\mathcal H}(V)=1_{\mathcal H}\otimes|0\rangle\langle0|+V\otimes|1\rangle\langle1|$ , $H=2^{-1/2}\begin{pmatrix}1&1\\1&-1\end{pmatrix}$ , and

E_\ell(s)=C_{\mathcal H}(e^{-isB_\ell})(1_{\mathcal H}\otimes H) C_{\mathcal H}(e^{-i\pi B_{\mathrm{none}}}).

For $h\in\Lambda^T$ and $s\in[0,1]^T$ , let $V_{h,s}$ apply $E_{h_j}(s_j)$ successively on $\mathcal H$ and ancilla $j$ , let $\eta_T=((|0\rangle-|1\rangle)/\sqrt2)^{\otimes T}$ , set $X_{h,s}=V_{h,s}(\rho\otimes\eta_T\eta_T^\dagger)V_{h,s}^\dagger$ , and set $\widehat V_{h,s}=(Z\otimes1)V_{h,s}(Z^\dagger\otimes1)$ . Define the matrix map

\mathcal M_{Z,T}(\rho)= \frac1{|\Lambda|^T}\sum_{h\in\Lambda^T}\int_{[0,1]^T} \operatorname{Tr}_{\mathrm{anc}}\!\left[ \widehat V_{h,s}^\dagger \left(Z\xi\xi^\dagger Z^\dagger\otimes\operatorname{Tr}_{\mathcal H}X_{h,s}\right) \widehat V_{h,s} \right]ds,

with entrywise Lebesgue integration and empty products interpreted as identities. For every such $U$ and every real $\varepsilon>0$ , there exists a natural number $N$ such that, for every $T\ge N$ and every positive semidefinite matrix $\rho$ on $\mathcal H$ of trace $1$ satisfying $\Pi_B\rho\Pi_B=\rho$ ,

\tfrac12\operatorname{Re}\operatorname{tr} \sqrt{(\mathcal M_{Z,T}(\rho)-Z\rho Z^\dagger)^\dagger (\mathcal M_{Z,T}(\rho)-Z\rho Z^\dagger)} \le\varepsilon.

The averaging family has $1+2|K|$ indices and includes the anchor index $\mathrm{none}$ .

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