Symmetric coherent information as a cq information difference

Open

QAlgorithms.Papers.Independent.Intakethird100.P10.coherentInformation_identity

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

prove2quantum

Let $U:\mathbb C^2\to B\otimes E$ be an isometry with finite nonempty output registers, and choose any orthonormal qubit input basis. Let $W$ and $W^*$ be the cq channels induced in that basis by tracing out $E$ and $B$ , respectively. Let $\omega^{AB}$ be obtained by sending the second half of the normalized Bell state through this same isometry and discarding $E$ . Then

I_{\mathrm c}^{\mathrm{sym}}(U):=H(\omega^B)-H(\omega^{AB})=I(W)-I(W^*).

All entropies are in bits. The register $A$ here is the retained Bell reference. Neither degradability nor commuting environment outputs are required, and no optimization over input density matrices occurs.

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.6–7, unnumbered identity: no degradation or commuting-environment assumption.
The normalized Bell input and the two cq channels use one orthonormal input basis. -/
theorem coherentInformation_identity {B E : Type*}
    [Fintype B] [DecidableEq B] [Nonempty B]
    [Fintype E] [DecidableEq E] [Nonempty E]
    (U : Matrix (B × E) Bool ℂ) (hU : Uᴴ * U = 1)
    (basis : Matrix.unitaryGroup Bool ℂ) :
    symmetricCoherentInformation U basis =
      symmetricInformation (dilationBob U basis) - symmetricInformation (dilationEve U basis) := by sorry

end QAlgorithms.Papers.Independent.Intakethird100.P10

end

Source

Polar codes for degradable quantum channels, arXiv:1109.5346v3, PDF p. 6, §IV, unnumbered symmetric coherent information identity

Read-back

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

Let $B,E$ be finite, nonempty sets with decidable equality, let $U$ be a complex matrix with rows indexed by $B\times E$ and Boolean columns satisfying $U^\dagger U=I_2$ , and let $Q$ be any unitary $2\times2$ matrix. Put $v_x(b,e)=\sum_{a\in\{0,1\}}U((b,e),a)Q(a,x)$ , $R_x(b,b')=\sum_e v_x(b,e)\overline{v_x(b',e)}$ , $T_x(e,e')=\sum_b v_x(b,e)\overline{v_x(b,e')}$ , and $\Omega((x,b),(y,b'))=\tfrac12\sum_e v_x(b,e)\overline{v_y(b',e)}$ . With $S(X)=-\operatorname{Re}\operatorname{tr}(f(X))$ , where $f(t)=t\log_2t$ is applied by continuous functional calculus, the assertion is

S\!\left(\frac{R_0+R_1}{2}\right)-S(\Omega) = \left[S\!\left(\frac{R_0+R_1}{2}\right)-\frac{S(R_0)+S(R_1)}2\right] - \left[S\!\left(\frac{T_0+T_1}{2}\right)-\frac{S(T_0)+S(T_1)}2\right].

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