II A: matrix coefficients and block decomposition, (3)–(4)

Open

QAlgorithms.Papers.Independent.Intakethird100.P30.updatedStateStructure

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

prove2quantum

Let $C=(C_k)_{k\in K}$ be a nonempty family of distinct $n$ -bit words, $n\ge1$ , and let $P_C(Q)$ be the Bob-only filtered six-state operator for $0\le Q\le\tfrac12$ . For $a,a'\in\{0,1\}^n$ , set $u=|a\oplus a'|$ and $v=|a\oplus C_k|$ , where $|\cdot|$ counts ones. Call an entry compatible when $a\oplus C_k=a'\oplus C_l$ and $(a\oplus C_k)\mathbin{\odot}(a\oplus a')=0^n$ , with $\odot$ bitwise AND. In that case $u+v\le n$ , and

P_C(Q)_{a,k;a',l}= \begin{cases} ((1-2Q)/2)^u(Q/2)^v((1-Q)/2)^{n-u-v},&\text{compatible},\\ 0,&\text{otherwise}. \end{cases}

The fixed permutation $V|a,k\rangle=|a\oplus C_k,k\rangle$ is unitary and satisfies

VP_C(Q)V^\dagger=\bigoplus_{\beta\in\{0,1\}^n}M_\beta, \qquad (M_\beta)_{kl}=P_C(Q)_{\beta\oplus C_k,k;\beta\oplus C_l,l}.

Both compatibility conditions are retained, so sector agreement alone is not asserted to make an entry nonzero.

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.3, (3)–(4): both delta guards, compatible exponents, and actual unitary
block decomposition. No extra factor 2^(-n), and no erroneous nonzero iff. -/
theorem updatedStateStructure {n : ℕ} (hn : 1 ≤ n) [Nonempty K]
    (C : K → Qubits n) (hC : Function.Injective C) (Q : ℝ)
    (hQ0 : 0 ≤ Q) (hQ1 : Q ≤ 1 / 2) :
    (∀ (a a2 : Qubits n) (k l : K),
      (MatrixEntryCompatible C a a2 k l → hammingDist a a2 + hammingDist a (C k) ≤ n) ∧
      bobState C Q (a, k) (a2, l) =
        if MatrixEntryCompatible C a a2 k l then
          ((((1 - 2 * Q) / 2) ^ hammingDist a a2 *
            (Q / 2) ^ hammingDist a (C k) *
            ((1 - Q) / 2) ^ (n - hammingDist a a2 - hammingDist a (C k)) : ℝ) : ℂ)
        else 0) ∧
    (xorSectorPermutation C)ᴴ * xorSectorPermutation C = 1 ∧
    xorSectorPermutation C * (xorSectorPermutation C)ᴴ = 1 ∧
    (∀ p q, (xorSectorPermutation C * bobState C Q * (xorSectorPermutation C)ᴴ) p q =
      if p.1 = q.1 then xorSectorBlock C Q p.1 p.2 q.2 else 0) := 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. 3, II A: matrix coefficients and block decomposition, (3)–(4)

Read-back

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

Let $n\ge1$ , let $K$ be a finite nonempty label type with the required decidable equality, let $C:K\to\{0,1\}^{n}$ be injective, and let $0\le Q\le1/2$ . Write $d(a,b)$ for the number of coordinates at which two Boolean strings differ, and define

B_{C,Q}((a,k),(a',l)) =\prod_{i=0}^{n-1} \left( \frac{1-2Q}{2}\mathbf1_{a_i=C(k)_i}\mathbf1_{a'_i=C(l)_i} +\frac Q2\mathbf1_{a_i=a'_i}\mathbf1_{C(k)_i=C(l)_i} \right).

Call $(a,a',k,l)$ compatible when $a\oplus C(k)=a'\oplus C(l)$ and no coordinate has both $a_i\oplus C(k)_i=1$ and $a_i\oplus a'_i=1$ . The theorem asserts, for every $a,a',k,l$ , that compatibility implies $d(a,a')+d(a,C(k))\le n$ , and that

B_{C,Q}((a,k),(a',l)) = \begin{cases} \displaystyle \left(\frac{1-2Q}{2}\right)^{d(a,a')} \left(\frac Q2\right)^{d(a,C(k))} \left(\frac{1-Q}{2}\right)^{n-d(a,a')-d(a,C(k))}, &\text{if compatible},\\ 0,&\text{otherwise}, \end{cases}

where the displayed real value is embedded in $\mathbb C$ . Natural-number subtraction is truncated at zero; the stated bound prevents truncation in the compatible case, and every zeroth power, including $0^0$ , is $1$ . Define $P_C((a,k),(b,l))=1$ when $a=b\oplus C(l)$ and $k=l$ , and $0$ otherwise, and define $H_{C,Q,\beta}(k,l)=B_{C,Q}((\beta\oplus C(k),k),(\beta\oplus C(l),l))$ . The theorem also asserts

P_C^\dagger P_C=I,\qquad P_CP_C^\dagger=I,\qquad (P_CB_{C,Q}P_C^\dagger)_{(\beta,k),(\gamma,l)} = \begin{cases} H_{C,Q,\beta}(k,l),&\beta=\gamma,\\ 0,&\beta\ne\gamma. \end{cases}

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