§III A, Eq.(21): distortion-free factorization

Open

QAlgorithms.Papers.Independent.Intakethird100.P67.distortion_free

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

prove2quantum

Fix normalized pure samples generating the full supported algebra, an anchor, $K\ge2$ , and $T\ge0$ . Construct $\mathcal E_I$ by the same Appendix-A emulator with target equal to the identity. For every ambient unitary $U$ and input density operator $\rho$ ,

\mathcal E_U(\rho)=U\mathcal E_I(\rho)U^\dagger.

Thus the distortion channel is fixed by the input samples before $U$ is chosen. It is the constructed main-system channel, rather than an arbitrary channel selected afterward or the outcome-dependent discarded SWAP wire.

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.6, Eq.(21): factorization through the constructed target-I channel. -/
theorem distortion_free (phi : K → EuclideanSpace ℂ I) (a : K) (hK : 2 ≤ Fintype.card K)
    (hphi : ∀ k, IsState (phi k)) (hgen : Generates (pureSamples phi)) (T : ℕ) :
    ∀ U : Matrix.unitaryGroup I ℂ, ∀ rho : Matrix I I ℂ, IsDensityMatrix rho →
      emulate phi a (U : Matrix I I ℂ) T rho = densityConjugation (U : Matrix I I ℂ) (emulate phi a 1 T rho) := by sorry

end QAlgorithms.Papers.Independent.Intakethird100.P67

end

Source

Universal Quantum Emulator, arXiv:1606.02734v2, PDF p. 6, §III A, Eq.(21): distortion-free factorization

Read-back

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

Let $I,K$ be finite types with decidable equality, let $|K|\ge2$ , choose $a\in K$ , and let $\phi_k\in\mathbb C^I$ have norm $1$ for every $k$ . Set $S_k=|\phi_k\rangle\langle\phi_k|$ , $\Pi=f(\sum_kS_k)$ , where continuous functional calculus uses $f(0)=0$ and $f(t)=1$ otherwise, and suppose that the complex span of all nonempty finite products of the $S_k$ is exactly $\{X:\Pi X\Pi=X\}$ . For any natural number $T$ , define $p_a=0$ and $p_k=(|K|-1)^{-1}$ for $k\ne a$ , $R_k=1-2S_k$ , and $W_k=C(R_k)(1\otimes H)C(R_a)$ , where $C(R)$ applies $R$ precisely when its Boolean ancilla is true and $H=2^{-1/2}\begin{pmatrix}1&1\\1&-1\end{pmatrix}$ . Put $\mu_T=|-\rangle\langle-|^{\otimes T}$ , with $|-\rangle=(|0\rangle-|1\rangle)/\sqrt2$ ; for each history $h:\{0,\ldots,T-1\}\to K$ , let $p_h=\prod_{j<T}p_{h(j)}$ , let $H_h$ apply $W_{h(j)}$ to the system and ancilla $j$ in increasing order of $j$ , and define $H_h^{(V)}=(V\otimes1)H_h(V^\dagger\otimes1)$ . With $Q_{\mathrm{false}}=S_a$ and $Q_{\mathrm{true}}=1-S_a$ , define

\mathcal M_V(\rho)= \operatorname{Tr}_{\mathrm{anc}} \sum_{b\in\{\mathrm{false},\mathrm{true}\}}\sum_h p_h\, H_h^{(V)\dagger} \left[ |V\phi_a\rangle\langle V\phi_a|\otimes \operatorname{Tr}_{I}\!\left( (Q_b\otimes1)H_h(\rho\otimes\mu_T)H_h^\dagger(Q_b\otimes1)^\dagger \right) \right]H_h^{(V)}.

Then, for every unitary matrix $U$ on $I$ and every positive semidefinite trace-one matrix $\rho$ on $I$ ,

\mathcal M_U(\rho)=U\,\mathcal M_1(\rho)\,U^\dagger.

There is no requirement that $\rho$ satisfy $\Pi\rho\Pi=\rho$ . The case $T=0$ is included, using the single empty history with weight $1$ , identity history matrix, and a one-dimensional empty ancilla register.

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