II B: code equivalence preserves updated states and thresholds, (7)

Open

QAlgorithms.Papers.Independent.Intakethird100.P30.equivalentCodes

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

prove2quantum

Let $C$ and $D$ be nonempty codes of distinct $n$ -bit words, $n\ge1$ . Suppose a permutation of coordinates followed by XOR with one fixed binary word maps their underlying code sets onto one another; word enumeration is immaterial. Let $P_C(Q)$ and $P_D(Q)$ denote their Bob-only filtered six-state operators. There are local permutation unitaries $U$ on Alice and $V$ between the code-label registers, chosen independently of $Q$ , such that

P_C(Q)=(U\otimes V)P_D(Q)(U\otimes V)^\dagger \quad\text{for every }0\le Q\le\tfrac12.

Consequently the two operators are symmetrically extendable for exactly the same QBERs, and

Q_C^*=Q_D^*.

This is the fixed-basis interpretation of the source's equality: changing word order or coordinate labels changes matrix coefficients by local unitaries.

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 pp.3–4, (7): equality means local permutation conjugacy, independently
of Q. Printed raw matrix equality is corrected using p.3's ordering convention. -/
theorem equivalentCodes {n : ℕ} (hn : 1 ≤ n) [Nonempty K] [Nonempty L]
    (C : K → Qubits n) (D : L → Qubits n)
    (hC : Function.Injective C) (hD : Function.Injective D)
    (hCD : CodeEquivalent C D) :
    (∃ (u : Equiv.Perm (Qubits n)) (v : L ≃ K),
      let U : Matrix (Qubits n) (Qubits n) ℂ := fun a b => if a = u b then 1 else 0
      let V : Matrix K L ℂ := fun k l => if k = v l then 1 else 0
      Uᴴ * U = 1 ∧ U * Uᴴ = 1 ∧ Vᴴ * V = 1 ∧ V * Vᴴ = 1 ∧
      ∀ Q : ℝ, 0 ≤ Q → Q ≤ 1 / 2 →
        bobState C Q = Matrix.kronecker U V * bobState D Q * (Matrix.kronecker U V)ᴴ) ∧
    (∀ Q : ℝ, 0 ≤ Q → Q ≤ 1 / 2 →
      (BobExtendible (bobState C Q) ↔ BobExtendible (bobState D Q))) ∧
    bobThreshold C = bobThreshold D := 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. 4, II B: code equivalence preserves updated states and thresholds, (7)

Read-back

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

Let $n\ge1$ , let $K,L$ be finite nonempty label types with the required decidable equality, and let $C:K\to\{0,1\}^{n}$ and $D:L\to\{0,1\}^{n}$ be injective. Assume there exist a coordinate permutation $p$ , a Boolean mask $t$ , and a bijection $e:K\to L$ such that $C(k)_i=D(e(k))_{p(i)}\oplus t_i$ for every $k,i$ . For either code $E$ , define

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

The theorem asserts the existence of a permutation $u$ of all $n$ -bit strings and a bijection $v:L\to K$ such that the matrices $U_{a,b}=\mathbf1_{a=u(b)}$ and $V_{k,l}=\mathbf1_{k=v(l)}$ satisfy

U^\dagger U=UU^\dagger=I,\qquad V^\dagger V=VV^\dagger=I,

and, for every $Q\in[0,1/2]$ ,

B_{C,Q}=(U\otimes V)B_{D,Q}(U\otimes V)^\dagger.

For every such $Q$ , it also asserts that $B_{C,Q}$ admits a Bob-copy extension if and only if $B_{D,Q}$ does, where such an extension is a positive semidefinite matrix on an additional copy of the label subsystem with both label-copy partial traces equal to the original matrix, without a trace-one requirement. Finally, it asserts $b(C)=b(D)$ , where

b(E)=\sup\!\left(\{0\}\cup \{q\in[0,1/2]:B_{E,q}\text{ admits no Bob-copy extension}\}\right).

The same $u,v$ work for every $Q$ in the stated interval.

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