Fidelity transform and improvement of total root reliability

Open

QAlgorithms.Papers.Independent.Intakethird100.P14.fidelity_transform

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

prove2quantum

Let $W$ be any binary-input classical–quantum channel with normalized density outputs, and let $W^-$ and $W^+$ be the actual transforms (14)–(15), including the uniform classical flag for $W^+$ . For squared fidelity $F$ , all of the following hold:

\sqrt{F(W^+)}=F(W),\qquad \sqrt{F(W^-)}\le2\sqrt{F(W)}-F(W),\qquad F(W^-)\ge F(W)\ge F(W^+),

\sqrt{F(W^-)}+\sqrt{F(W^+)}\le2\sqrt{F(W)}.

The last display is the immediate consequence on page 8. The endpoints $F(W)=0$ and $F(W)=1$ are included. The final prose on page 12 reverses the last ordering; the formalization retains numbered (23), consistent with $F(W^+)=F(W)^2$ . These relations control reliability throughout the polarization tree.

Preamble

import Definitions.Def_QAlgorithms_Papers_Independent_Intakethird100_P14

Formal statement

noncomputable section

namespace QAlgorithms.Papers.Independent.Intakethird100.P14

open Filter MeasureTheory

open scoped ENNReal NNReal ComplexOrder BigOperators

open QAlgorithms.RealRegisters (Hilbert)

open QAlgorithms.Papers.Independent.Dependency50.P33 (IsDensity)

open QAlgorithms.Papers.Independent.Dependency50.P13 (compression)

open QAlgorithms.Papers.Independent.Renew46.P44 (wordOutput)

attribute [local instance] Classical.propDecidable Classical.decEq

/-- Proposition 9, (21)–(23), PDF p.7, and consequence p.8; proof pp.11–12.
The last prose inequality on p.12 is reversed; we retain numbered (23), as
also fixed by F(W+)=F(W)^2. Endpoints F=0 and F=1 are included. -/
theorem fidelity_transform {I : Type} (W : Bit → OutputCoefficients I) (hW : IsBinaryCqChannel W) :
    Real.sqrt (squaredCqFidelity (channelPlus W)) = squaredCqFidelity W ∧
    Real.sqrt (squaredCqFidelity (channelMinus W)) ≤
      2 * Real.sqrt (squaredCqFidelity W) - squaredCqFidelity W ∧
    squaredCqFidelity W ≤ squaredCqFidelity (channelMinus W) ∧
    squaredCqFidelity (channelPlus W) ≤ squaredCqFidelity W ∧
    Real.sqrt (squaredCqFidelity (channelMinus W)) + Real.sqrt (squaredCqFidelity (channelPlus W)) ≤
      2 * Real.sqrt (squaredCqFidelity W) := by sorry

end QAlgorithms.Papers.Independent.Intakethird100.P14

end

Source

Polar codes for classical-quantum channels, arXiv:1109.2591v3, PDF p. 7, Proposition 9: fidelity transformation

Read-back

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

Let $I$ be any type and let $W_b$ , $b\in\mathbb F_2$ , be density coefficient arrays: each has a countable expansion $W_b(i,j)=\sum_r u_r(i)\overline{v_r(j)}$ with $u_r,v_r\in\ell^2(I;\mathbb C)$ and $\sum_r\|u_r\|\|v_r\|<\infty$ , all finite quadratic forms are real and nonnegative, and the real diagonal is summable with sum $1$ . For any array $X$ , let $O(X)$ be a chosen bounded operator with those coordinate coefficients if one exists, and $0$ otherwise. For any bounded operator $T$ , let $R(T)$ be a chosen positive bounded square root if one exists, and $0$ otherwise. Put $\operatorname{tr}_bT=\sum_j(Te_j)_j$ , using the total infinite sum, and define

F(V)=\left[\operatorname{Re}\operatorname{tr}_b R\!\left(R(O(V_0))\,O(V_1)\,R(O(V_0))\right)\right]^2

for a binary array $V$ . Define $W_b^-((a_1,a_2),(c_1,c_2))=\tfrac12\sum_{d\in\mathbb F_2}W_{b+d}(a_1,c_1)W_d(a_2,c_2)$ , and define $W_d^+((b,(a_1,a_2)),(b',(c_1,c_2)))=\mathbf1_{b=b'}\tfrac12W_{b+d}(a_1,c_1)W_d(a_2,c_2)$ , with bit addition modulo $2$ . Then

\sqrt{F(W^+)}=F(W),\qquad \sqrt{F(W^-)}\le2\sqrt{F(W)}-F(W),\qquad F(W)\le F(W^-),\qquad F(W^+)\le F(W), \qquad \sqrt{F(W^-)}+\sqrt{F(W^+)}\le2\sqrt{F(W)}.

All five conclusions hold simultaneously. No countability or finite-dimensionality assumption on $I$ is made; a basis trace is assigned the value $0$ when its coefficient family is not summable.

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