II B / III C: unique two-word code without constant columns

Open

QAlgorithms.Papers.Independent.Intakethird100.P30.twoWordClassification

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

prove2quantum

Let $n\ge1$ and let $C=\{u,v\}$ consist of two distinct binary words. Put $d=|u\oplus v|$ , their Hamming distance, so $d\ge1$ . Write $R_j=\{0^j,1^j\}$ for the repetition code, and $Q_C^*$ for the Bob-only symmetric-extendability threshold of its constructed filtered family. Deleting constant coordinates produces a code equivalent to $R_d$ , and

Q_C^*=Q_{R_d}^*\le Q_{R_n}^*.

If $C$ already has no constant columns, it is equivalent to $R_n$ and its threshold equals $Q_{R_n}^*$ . Thus repetition codes are optimal among two-word codes at the same block length, including the valid one-bit case. This statement does not assert optimality among codes of other sizes.

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.4,6: classification and optimality among two-word codes, including
n=1 and reduction to positive Hamming distance after constant-column deletion. -/
theorem twoWordClassification {n : ℕ} (hn : 1 ≤ n)
    (C : Bool → Qubits n) (hC : Function.Injective C) :
    (NoConstantColumns C → CodeEquivalent C (repetition (Fin n)) ∧
      bobThreshold C = bobThreshold (repetition (Fin n))) ∧
    1 ≤ hammingDist (C false) (C true) ∧
    CodeEquivalent (deleteConstants C)
      (repetition (Fin (hammingDist (C false) (C true)))) ∧
    bobThreshold C = bobThreshold (repetition (Fin (hammingDist (C false) (C true)))) ∧
    bobThreshold C ≤ bobThreshold (repetition (Fin n)) := 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. 6, II B / III C: unique two-word code without constant columns

Read-back

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

Let $n\ge1$ and let $C:\{0,1\}\to\{0,1\}^{n}$ be injective. Write $d$ for the Hamming distance between $C(0)$ and $C(1)$ , let $V=\{i:\exists k,l,\ C(k)_i\ne C(l)_i\}$ , and let $C_V$ be the restriction of $C$ to $V$ . For any coordinate type $J$ , let $R_J(b)_i=b$ be the repetition code. Two codes $E:L\to\{0,1\}^{J}$ and $F:L'\to\{0,1\}^{J'}$ are called equivalent here precisely when there are bijections $p:J\to J'$ and $e:L\to L'$ and a Boolean mask $t:J\to\{0,1\}$ such that $E(k)_i=F(e(k))_{p(i)}\oplus t_i$ for all $k,i$ . Define

B_{E,Q}((a,k),(a',l)) =\prod_{i\in J} \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),

and let $b(E)$ be the supremum of $\{0\}$ together with the $q\in[0,1/2]$ for which $B_{E,q}$ has no positive semidefinite extension to an additional copy of its label subsystem with both label-copy partial traces equal to $B_{E,q}$ , without requiring trace one. The theorem asserts that if every coordinate of $C$ varies between some two labels, then $C$ is equivalent to $R_{\{0,\ldots,n-1\}}$ and their $b$ -values agree. It further asserts, without that additional condition, that

d\ge1,\qquad C_V\text{ is equivalent to }R_{\{0,\ldots,d-1\}},\qquad b(C)=b(R_{\{0,\ldots,d-1\}}),\qquad b(C)\le b(R_{\{0,\ldots,n-1\}}).

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