Proposition 4: continuous SWAP coupling approximates density-matrix evolution

Open

QAlgorithms.Papers.Independent.Intakethird100.P67.proposition4_continuous_swap

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

prove2quantum

Prepare $n\ge1$ independent reference registers in the same unit vector $\phi$ , a system density operator $\rho$ , a real coupling $J$ , and time $t\ge0$ . Let $H=J\sum_{j=1}^n\operatorname{SWAP}_{S,j}$ , $H_{\rm eff}=J(n+1)|\phi\rangle\langle\phi|$ , and let $\rho(t)$ be the actual system partial trace of the joint evolution. Then

F(\rho(t),e^{-itH_{\rm eff}}\rho e^{itH_{\rm eff}})\ge\frac{n-1}{n+1},\qquad\tfrac12\|\rho(t)-e^{-itH_{\rm eff}}\rho e^{itH_{\rm eff}}\|_1\le\frac6n.

For every normalized pure system input $\psi$ , the absolute overlap of $e^{-itH}(|\psi\rangle|\phi\rangle^{\otimes n})$ with $(e^{-itH_{\rm eff}}|\psi\rangle)|\phi\rangle^{\otimes n}$ is at least $(n-1)/(n+1)$ . These joint and reduced bounds refer to the same physical evolution.

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.24, Proposition 4, E4–E6: both reduced-state estimates and the absolute
joint overlap. Real subtraction prevents truncation at n=1; n=0 is excluded. -/
theorem proposition4_continuous_swap (phi : EuclideanSpace ℂ I) (hphi : IsState phi)
    (n : ℕ) (hn : 1 ≤ n) (coupling t : ℝ) (ht : 0 ≤ t) :
    (∀ rho : Matrix I I ℂ, IsDensityMatrix rho →
      let actual := traceRight (swapJoint phi n coupling t rho)
      let target := densityConjugation (positivePhaseEvolution (effectiveHamiltonian phi n coupling) (-t)) rho
      ((n : ℝ) - 1) / (n + 1) ≤ rootFidelity actual target ∧ traceDistance actual target ≤ 6 / n) ∧
    (∀ psi : EuclideanSpace ℂ I, IsState psi → ((n : ℝ) - 1) / (n + 1) ≤
      ‖inner ℂ (tensorVec (act (positivePhaseEvolution (effectiveHamiltonian phi n coupling) (-t)) psi)
        (referenceVector phi n)) (act (positivePhaseEvolution (swapHamiltonian n coupling) (-t))
          (tensorVec psi (referenceVector phi n)))‖) := by sorry

end QAlgorithms.Papers.Independent.Intakethird100.P67

end

Source

Universal Quantum Emulator, arXiv:1606.02734v2, PDF p. 24, Proposition 4: continuous SWAP coupling approximates density-matrix evolution

Read-back

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

Let $I$ be a finite index type with decidable equality, let $\phi\in\mathbb C^I$ have norm $1$ , let $n\ge1$ be a natural number, let $c\in\mathbb R$ be arbitrary, and let $t\ge0$ . Put $P=\phi\phi^\dagger$ , $\Phi_n=\phi^{\otimes n}$ , $H_{\mathrm{eff}}=c(n+1)P$ , and $H_{\mathrm{swap}}=c\sum_{j=0}^{n-1}S_j$ , where $S_j$ swaps the system register with reference register $j$ : on basis labels it sends $(i,(x_\ell)_\ell)$ to $(x_j,(x_\ell)_{\ell\ne j},i\text{ at }j)$ . For every positive semidefinite matrix $\rho$ of trace $1$ , define

A=\operatorname{Tr}_{\mathrm{ref}}\!\left[ e^{-itH_{\mathrm{swap}}}(\rho\otimes\Phi_n\Phi_n^\dagger)e^{itH_{\mathrm{swap}}} \right], \qquad B=e^{-itH_{\mathrm{eff}}}\rho e^{itH_{\mathrm{eff}}}.

Then

\frac{n-1}{n+1} \le\operatorname{Re}\operatorname{tr}\sqrt{\sqrt A\,B\sqrt A}, \qquad \tfrac12\operatorname{Re}\operatorname{tr}\sqrt{(A-B)^\dagger(A-B)} \le\frac6n,

with square roots defined by functional calculus. In addition, for every norm- $1$ vector $\psi\in\mathbb C^I$ ,

\frac{n-1}{n+1} \le \left| \left\langle (e^{-itH_{\mathrm{eff}}}\psi)\otimes\Phi_n,\, e^{-itH_{\mathrm{swap}}}(\psi\otimes\Phi_n) \right\rangle \right|.

The case $n=1$ is included; no sign or magnitude restriction is imposed on $c$ , and there is no upper bound on $t$ .

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