Strict obstruction to the classical poor-channel inequality

Open

QAlgorithms.Papers.Independent.Intakethird100.P10.pureOutput_poor_inequality_fails

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

prove2quantum

Let $W$ have two normalized pure outputs on a finite nonempty register, with squared overlap strictly between zero and one. Construct $W^-$ from the even and odd parity mixtures in Appendix A. Write $f=\sqrt{F(W)}$ . Then

\sqrt{F(W^-)}=f<f\sqrt{2-f^2}.

Thus the lower bound in (10), valid for commuting-output channels, fails strictly here. This statement concerns that inequality and does not assert unattainability of a private information rate.

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 pp.5,10: strict failure of the classical poor-channel inequality (10)
for pure outputs whose squared overlap is strictly between zero and one.
Only failure of that inequality is asserted, not an impossibility of private coding. -/
theorem pureOutput_poor_inequality_fails {H : Type*}
    [Fintype H] [DecidableEq H] [Nonempty H]
    (psi0 psi1 : EuclideanSpace ℂ H) (h0 : IsState psi0) (h1 : IsState psi1)
    (hlo : 0 < ‖inner ℂ psi0 psi1‖ ^ 2) (hhi : ‖inner ℂ psi0 psi1‖ ^ 2 < 1) :
    let W := pureCQ psi0 psi1
    let M := minusChannel W
    let f := rootFidelity (W false) (W true)
    rootFidelity (M false) (M true) = f ∧
      rootFidelity (M false) (M true) < f * Real.sqrt (2 - f ^ 2) := by sorry

end QAlgorithms.Papers.Independent.Intakethird100.P10

end

Source

Polar codes for degradable quantum channels, arXiv:1109.5346v3, PDF p. 5, §III/Appendix A, unnumbered obstruction to the classical poor-channel inequality

Read-back

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

For every finite nonempty index type $H$ with decidable equality and unit vectors $\psi_0,\psi_1\in\mathbb C^H$ satisfying $0<|\langle\psi_0,\psi_1\rangle|^2<1$ , define $P_i=\psi_i\psi_i^*$ , $M_0=(P_0\otimes P_0+P_1\otimes P_1)/2$ , $M_1=(P_0\otimes P_1+P_1\otimes P_0)/2$ , and $f=R(P_0,P_1)$ , where

R(\rho,\sigma)=\operatorname{Re}\operatorname{tr} \sqrt{\sqrt{\rho}\,\sigma\,\sqrt{\rho}}

uses continuous functional calculus for the square roots. Then

R(M_0,M_1)=f \quad\text{and}\quad R(M_0,M_1)<f\sqrt{2-f^2}.

The overlap hypotheses exclude both orthogonal vectors and vectors with overlap of modulus $1$ ; in particular, no such pair exists when $H$ has just one element.

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