Prove2Me

Pure-output minus transform preserves squared fidelity

Open
QAlgorithms.Papers.Independent.Intakethird100.P10.pureOutput_minus_fidelity

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

prove2quantum

Let ∣ψ0⟩,∣ψ1⟩|\psi_0\rangle,|\psi_1\rangle be normalized vectors on a common finite nonempty register, and put W(x)=∣ψx⟩⟨ψx∣W(x)=|\psi_x\rangle\langle\psi_x|. Construct W−W^- with letter states

ρ0−=12(ρ0⊗ρ0+ρ1⊗ρ1),ρ1−=12(ρ0⊗ρ1+ρ1⊗ρ0).\rho_0^-={1\over2}(\rho_0\otimes\rho_0+\rho_1\otimes\rho_1),\qquad \rho_1^-={1\over2}(\rho_0\otimes\rho_1+\rho_1\otimes\rho_0).

Then the squared Uhlmann fidelities satisfy

F(W)=∣⟨ψ0∣ψ1⟩∣2=F(W−).F(W)=|\langle\psi_0|\psi_1\rangle|^2=F(W^-).

Distinctness and orthogonality are not assumed. This equality identifies why the classical poor-channel inequality can fail for quantum pure outputs.

Preamble
import Definitions.Def_QAlgorithms_Papers_Independent_Intakethird100_P10
Formal statement
noncomputable section

namespace QAlgorithms.Papers.Independent.Intakethird100.P10

open scoped BigOperators Matrix ComplexConjugate

open Filter

-- Accepted definitions, without paper-local aliases.

open QAlgorithms.Papers.Independent.Information100.P58 (basisDensity)

open QAlgorithms.Papers.Independent.Information100.P67 (squaredFidelity)

open QAlgorithms.Papers.Independent.Claimed50.P48 (indexedKrausDilation)

/-- PDF p.10, Theorem 9: squared fidelity is squared overlap for pure letters,
and is unchanged by the explicitly constructed worse branch.
Coincident and orthogonal normalized vectors are both allowed. -/
theorem pureOutput_minus_fidelity {H : Type*} [Fintype H] [DecidableEq H] [Nonempty H]
    (psi0 psi1 : EuclideanSpace ℂ H) (h0 : IsState psi0) (h1 : IsState psi1) :
    squaredFidelity (pureCQ psi0 psi1 false) (pureCQ psi0 psi1 true) = ‖inner ℂ psi0 psi1‖ ^ 2 ∧
    squaredFidelity (pureCQ psi0 psi1 false) (pureCQ psi0 psi1 true) =
      squaredFidelity (minusChannel (pureCQ psi0 psi1) false)
        (minusChannel (pureCQ psi0 psi1) true) := by sorry

end QAlgorithms.Papers.Independent.Intakethird100.P10

end
Source
Polar codes for degradable quantum channels, arXiv:1109.5346v3, PDF p. 10, Theorem 9: pure-output minus transform preserves fidelity
Read-back

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

For every finite nonempty index type HH with decidable equality and every pair of vectors ψ0,ψ1∈CH\psi_0,\psi_1\in\mathbb C^H satisfying ∥ψ0∥=∥ψ1∥=1\|\psi_0\|=\|\psi_1\|=1, put Pi=ψiψi∗P_i=\psi_i\psi_i^*, M0=(P0⊗P0+P1⊗P1)/2M_0=(P_0\otimes P_0+P_1\otimes P_1)/2, and M1=(P0⊗P1+P1⊗P0)/2M_1=(P_0\otimes P_1+P_1\otimes P_0)/2. Then

F(P0,P1)=∣⟨ψ0,ψ1⟩∣2andF(P0,P1)=F(M0,M1),F(P_0,P_1)=|\langle\psi_0,\psi_1\rangle|^2 \quad\text{and}\quad F(P_0,P_1)=F(M_0,M_1),

where

F(ρ,σ)=(Re⁡tr⁡ρ σ ρ)2,F(\rho,\sigma)= \left(\operatorname{Re}\operatorname{tr} \sqrt{\sqrt{\rho}\,\sigma\,\sqrt{\rho}}\right)^2,

with matrix square roots evaluated by continuous functional calculus.

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