Coherent polar encoder and reversed phase side information

Open

QAlgorithms.Papers.Independent.Intakethird100.P74.phase_encoder_duality

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

prove2quantum

Let $\mathcal N:A'\to BE$ be a memoryless finite-register quantum wiretap channel with qubit input, with a fixed isometric extension $V:A'\to BES_2$ . Choose two unit purifications $|\psi_z\rangle^{A'S_1}$ of the input states, with $z\in\{0,1\}$ equiprobable. Both shields $S_1,S_2$ are excluded from Eve. Let $W_{A,B}$ and $W_{A,E}$ be the resulting amplitude channels to Bob and Eve. The virtual phase channel $W_{P,B}$ has output $BCS_1S_2$ , obtained by phase modulating the reference of the coherent source $2^{-1/2}\sum_z|z\rangle^C|\psi_z\rangle$ and tracing only Eve after $V$ . Entropies and Holevo information are in bits, and $F$ denotes squared fidelity.

For $N=2^n$ and a phase input row vector $x^N$ , form the coherent output

|\Omega_{x^N}\rangle=2^{-N/2}\sum_{z^N}(-1)^{x^N\cdot z^N} |\psi_{z^N G_N}\rangle^{B^NE^NS_1^NS_2^N}|z^N\rangle^{C^N},

where the signal vector is the product of the one-use purified outputs. Let $\omega_{y^N}=\bigotimes_j\omega_{y_j}$ be the product virtual phase output and let $U_E^{C^N}$ be the polar encoder acting only on the reference register. Then

\operatorname{Tr}_{E^N}|\Omega_{x^N}\rangle\langle\Omega_{x^N}| =U_E^{C^N}\omega_{x^N G_N^T}(U_E^{C^N})^\dagger.

For each index, the split state obtained by revealing future phase bits and averaging earlier phase bits equals the corresponding split of the transposed product phase channel, conjugated by the same reference encoder. This supplies the phase construction used for the polar good-index sets.

Preamble

import Definitions.Def_QAlgorithms_Papers_Independent_Intakethird100_P74

Formal statement

namespace QAlgorithms.Papers.Independent.Intakethird100.P74

open QAlgorithms

open scoped ComplexConjugate Matrix

noncomputable section

local instance (p : Prop) : Decidable p := Classical.propDecidable p

variable {B E S1 S2 : Type}

variable [Fintype B] [Fintype E] [Fintype S1] [Fintype S2]

variable [DecidableEq B] [DecidableEq E] [DecidableEq S1] [DecidableEq S2]

/-- PDF pp.3–4, §II.B: row-vector x G_N^T and extra conjugation on C^N.
The second equality spells out the future-bit side information of phase splitting. -/
theorem phase_encoder_duality (d : WiretapData B E S1 S2) (hd : d.Valid) :
    (∀ (n : ℕ) (x : Qubits (2 ^ n)), encodedPhaseOutput d n x =
      referenceEncoder d n * QAlgorithms.Papers.Independent.Information100.P56.productOutput (2 ^ n) (phaseBob d) (polarEncode n true x) *
        (referenceEncoder d n)ᴴ) ∧
    (∀ (n : ℕ) (i : Fin (2 ^ n)) (b : Bool), actualPhaseSplit d n i b =
      idTensorSuperop (conjSuperop (referenceEncoder d n))
        (splitOutput n true (phaseBob d) i b)) := by sorry

end

end QAlgorithms.Papers.Independent.Intakethird100.P74

Source

Polar codes for private classical communication, arXiv:1203.5794v1, PDF p. 3, §II.B, unnumbered: coherent polar encoder and reversed phase side information

Read-back

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

For finite index types $B,E,S_1,S_2$ , with decidable equality as required, let $d=(V,\psi)$ satisfy $V^*V=I_2$ and $\|\psi_z\|=1$ for both Boolean $z$ . Put

s_z(b,e,s,t)=\sum_{a\in\{0,1\}}V_{(b,e,t),a}\psi_z(a,s),\quad \varphi_x((z,b,s,t),e)=2^{-1/2}(-1)^{xz}s_z(b,e,s,t),\quad W_x=\operatorname{Tr}_E(\varphi_x\varphi_x^*).

For every natural $n$ , including zero, write $N=2^n$ , $I=\{0,\ldots,N-1\}$ , and $H=\{0,1\}\times B\times S_1\times S_2$ . Define $G_{ij}=1$ if and only if every bit $k<n$ set in $j$ has bit $n-1-k$ set in $i$ , and define $e_-(u)_j=\sum_i u_iG_{ij}\pmod2$ and $e_+(u)_j=\sum_i u_iG_{ji}\pmod2$ . Let $R$ be the matrix on $H^I$ with entry $R_{y,z}=1$ exactly when the $B,S_1,S_2$ components of $y_i,z_i$ agree for every $i$ , and the Boolean components obey $y^{\mathrm{bit}}=e_-(z^{\mathrm{bit}})$ ; all other entries are zero. For each Boolean string $x\in\{0,1\}^I$ , define a vector on $H^I\times E^I$ by

\Xi_x(p,e)=2^{-N/2}(-1)^{\sum_i x_i z_i} \prod_{i\in I} s_{e_-(z)_i}\bigl((p_i)_B,e_i,(p_i)_{S_1},(p_i)_{S_2}\bigr), \qquad z_i=(p_i)_{\mathrm{bit}},

and set $E_x=\operatorname{Tr}_{E^I}(\Xi_x\Xi_x^*)$ . The first assertion is

E_x=R\left(\bigotimes_{i\in I}W_{e_+(x)_i}\right)R^* \quad\text{for every }n\text{ and }x.

The second assertion concerns every $i\in I$ and Boolean $b$ . Let $J_i=\{j\in I:i<j\}$ and define matrices $A_{i,b}$ and $\Sigma_{i,b}$ , indexed by $(h,y)\in\{0,1\}^{J_i}\times H^I$ , by

[A_{i,b}]_{(h,y),(h',y')}= \begin{cases} 2^{-(N-1)}\displaystyle\sum_{\substack{x_i=b\\x|_{J_i}=h}}(E_x)_{y,y'},&h=h',\\ 0,&h\ne h', \end{cases}

[\Sigma_{i,b}]_{(h,y),(h',y')}= \begin{cases} 2^{-(N-1)}\displaystyle\sum_{\substack{u_i=b\\u|_{J_i}=h}} \prod_{\ell\in I}W_{e_+(u)_\ell}(y_\ell,y'_\ell),&h=h',\\ 0,&h\ne h'. \end{cases}

Then $A_{i,b}=\mathcal C_R(\Sigma_{i,b})$ , where $\mathcal C_R$ acts on each block with fixed side-register row and column labels by $X^{h,h'}\mapsto RX^{h,h'}R^*$ . Thus this operation leaves those side-register labels in place.

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