IV A: Bell-diagonal structure of same-code simplex postselection, (21)–(22)

Open

QAlgorithms.Papers.Independent.Intakethird100.P30.simplexBellForm

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

prove2quantum

Let $C=(C_k)_{k=0}^{m-1}$ be distinct binary words of length $n\ge1$ , with $m\ge2$ , such that every pair of distinct words has Hamming distance $d$ , where $1\le d\le n$ . For $0\le Q\le\tfrac12$ , let $P$ be the operator after both parties filter the six-state input on $C$ . Put $s=((1-Q)/2)^n$ , $u=Q^d(1-Q)^{n-d}/2^n$ , $v=(1-2Q)^d(1-Q)^{n-d}/2^n$ , and $Z=ms+m(m-1)u$ . Then $\operatorname{Tr}P=Z>0$ . For the orthonormal Bell basis $|\Phi_{kl}\rangle=(I\otimes X^kZ^l)m^{-1/2}\sum_j|j,j\rangle$ , using cyclic shift and positive clock phase,

\frac{P}{Z}=\sum_{k,l}x_{kl}|\Phi_{kl}\rangle\langle\Phi_{kl}|, \quad x_{00}=a=\frac{s+(m-1)v}{Z},\quad x_{0l}=b=\frac{s-v}{Z}\ (l\ne0),\quad x_{kl}=\frac{u}{Z}=\frac{1-a-(m-1)b}{m(m-1)}\ (k\ne0).

These are actual eigenvalues, with $a\ge b\ge0$ and $a+(m-1)b\le1$ . Thus there are at most three eigenvalues, with degeneracy allowed. Normalization is explicit, and the coefficients are constructed from the code parameters rather than supplied as free hypotheses.

Preamble

import Definitions.Def_QAlgorithms_Papers_Independent_Intakethird100_P30

Formal statement

noncomputable section

namespace QAlgorithms.Papers.Independent.Intakethird100.P30

open scoped BigOperators Matrix ComplexConjugate ComplexOrder

attribute [local instance] Classical.propDecidable Classical.decEq

variable {I J K L A B : Type}

variable [Fintype I] [Fintype J] [Fintype K] [Fintype L]

variable [Fintype A] [Fintype B]

/-- PDF p.8, (21)–(22): the normalized, constructed same-code simplex operator
is Bell diagonal, with the three explicitly computed spectral sectors. -/
theorem simplexBellForm {n m d : ℕ} (hn : 1 ≤ n) (hm : 2 ≤ m)
    (hd0 : 1 ≤ d) (hdn : d ≤ n) (C : Fin m → Qubits n)
    (hC : Function.Injective C) (hd : Equidistant C d)
    (Q : ℝ) (hQ0 : 0 ≤ Q) (hQ1 : Q ≤ 1 / 2) :
    0 < simplexZ n m d Q ∧
    (bothState C Q).trace = (simplexZ n m d Q : ℂ) ∧
    IsDensityMatrix (((simplexZ n m d Q)⁻¹ : ℂ) • bothState C Q) ∧
    (((simplexZ n m d Q)⁻¹ : ℂ) • bothState C Q =
      ∑ k : Fin m, ∑ l : Fin m,
        (simplexWeights n m d Q k l : ℂ) • pureDensity (cyclicBellVector m k l)) ∧
    (∀ k l k2 l2 : Fin m,
      inner ℂ (cyclicBellVector m k l) (cyclicBellVector m k2 l2) =
        if k = k2 ∧ l = l2 then 1 else 0) ∧
    (∀ k l : Fin m, act (((simplexZ n m d Q)⁻¹ : ℂ) • bothState C Q) (cyclicBellVector m k l) =
      (simplexWeights n m d Q k l : ℂ) • cyclicBellVector m k l) ∧
    0 ≤ simplexB n m d Q ∧ simplexB n m d Q ≤ simplexA n m d Q ∧
    simplexA n m d Q + (m - 1) * simplexB n m d Q ≤ 1 ∧
    (∀ k l : Fin m, k.val ≠ 0 →
      simplexWeights n m d Q k l =
        (1 - simplexA n m d Q - (m - 1) * simplexB n m d Q) / (m * (m - 1))) := by sorry

end QAlgorithms.Papers.Independent.Intakethird100.P30

end

Source

Numerical evidence for bound secrecy from two-way post-processing in quantum key distribution, arXiv:1612.07734v2, PDF p. 8, IV A: Bell-diagonal structure of same-code simplex postselection, (21)–(22)

Read-back

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

For all natural numbers $n,m,d$ satisfying $n\ge1$ , $m\ge2$ , and $1\le d\le n$ , every injective map $C:\{0,\ldots,m-1\}\to\{0,1\}^n$ whose distinct indexed words have Hamming distance exactly $d$ , and every real $Q\in[0,\tfrac12]$ , define

S=\left(\frac{1-Q}{2}\right)^n,\qquad U=\frac{Q^d(1-Q)^{n-d}}{2^n},\qquad V=\frac{(1-2Q)^d(1-Q)^{n-d}}{2^n},\qquad Z=mS+m(m-1)U,

and put $a=(S+(m-1)V)/Z$ , $b=(S-V)/Z$ . For bits $u,v,u',v'$ , let

\sigma_Q((u,v),(u',v')) =\frac{1-2Q}{2}\mathbf1_{u=v}\mathbf1_{u'=v'} +\frac Q2\mathbf1_{u=u'}\mathbf1_{v=v'},

and define the matrix $P$ , indexed by pairs of word labels, by

P_{(r,s),(r',s')}=\prod_{i=0}^{n-1} \sigma_Q((C_r(i),C_s(i)),(C_{r'}(i),C_{s'}(i))).

For $k,l\in\{0,\ldots,m-1\}$ , define vectors and real weights by

v_{kl}(r,s)= \begin{cases} m^{-1/2}\exp(2\pi\mathrm{i}rl/m),&s=(r+k)\bmod m,\\ 0,&\text{otherwise}, \end{cases} \qquad w_{kl}= \begin{cases} a,&k=0,\ l=0,\\ b,&k=0,\ l\ne0,\\ U/Z,&k\ne0. \end{cases}

Then $Z>0$ , $\operatorname{tr}P=Z$ , and $\rho=Z^{-1}P$ is positive semidefinite with trace $1$ . Moreover,

\rho=\sum_{k=0}^{m-1}\sum_{l=0}^{m-1}w_{kl}\,v_{kl}v_{kl}^{*},\qquad \langle v_{kl},v_{k'l'}\rangle= \begin{cases}1,&k=k'\text{ and }l=l',\\0,&\text{otherwise},\end{cases} \qquad \rho v_{kl}=w_{kl}v_{kl}.

Here $vv^{*}$ has entries $v(x)\overline{v(y)}$ . Finally, $0\le b\le a$ , $a+(m-1)b\le1$ , and, for every $k\ne0$ and every $l$ ,

w_{kl}=\frac{1-a-(m-1)b}{m(m-1)}.

The endpoints $Q=0$ and $Q=\tfrac12$ are included.

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