III D: equivalence bound for adding one column

Open

QAlgorithms.Papers.Independent.Intakethird100.P30.columnExtension

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

prove2quantum

Let $C=(C_k)_{k\in\{0,\ldots,m-1\}}$ be a code of distinct $n$ -bit words, with $n\ge1$ , $m\ge2$ , and no constant columns. For a column $v\in\{0,1\}^m$ , let $C[v]$ be obtained by adjoining $v_k$ to word $C_k$ . A change between the first and last position of the new column is a coordinate permutation. Then

C[v]\sim C[\overline v],\qquad Q_{C[0^m]}^*=Q_{C[1^m]}^*=Q_C^*,

and the number of equivalence classes represented by the nonconstant new columns satisfies

\#\{[C[v]]:v\text{ is nonconstant}\}\le2^{m-1}-1.

Further coordinate equivalences may identify different complement pairs, so this is only an upper bound. The result asserts no improvement in the threshold from any particular new column.

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.7: complementary columns give equivalent codes, constant columns preserve
threshold, and at most 2^(m-1)-1 nonconstant-column equivalence classes remain. -/
theorem columnExtension {n m : ℕ} (hn : 1 ≤ n) (hm : 2 ≤ m)
    (C : Fin m → Qubits n) (hC : Function.Injective C) (hcols : NoConstantColumns C) :
    (∀ v : Fin m → Bool, CodeEquivalent (prependCodeColumn C v) (prependCodeColumn C (fun k => !(v k)))) ∧
    (∀ b : Bool, bobThreshold (prependCodeColumn C (fun _ => b)) = bobThreshold C) ∧
    (columnOrbitCandidates C).card ≤ 2 ^ (m - 1) - 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. 7, III D: equivalence bound for adding one column

Read-back

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

For natural numbers $n\ge1$ and $m\ge2$ , let $C$ be an injective collection of $m$ Boolean words of length $n$ , and assume that every coordinate takes different values on some two words of $C$ . Write $C_v(k)=(v_k,C(k))$ for a prepended Boolean column $v$ . The theorem asserts that for every $v$ , the collections $C_v$ and $C_{\neg v}$ are equivalent: there exist a coordinate permutation $p$ , a Boolean word $t$ of length $n+1$ , and a permutation $e$ of the $m$ labels such that $C_v(k)_i=C_{\neg v}(e(k))_{p(i)}\oplus t_i$ for every $k,i$ . It also asserts that prepending either constant Boolean column preserves the Bob threshold, and that the number of distinct coordinate-permutation-and-bit-flip orbits obtained from all varying prepended columns is at most $2^{m-1}-1$ ; each orbit is the set of all images of the underlying word set under $w_i\mapsto w_{p(i)}\oplus t_i$ . For a code $D:L\to\{0,1\}^{J}$ , its Bob threshold is the supremum of $\{0\}$ together with those $q\in[0,\tfrac12]$ for which the matrix

[P_D(q)]_{(a,k),(a',l)} =\prod_{i\in J}\left[ \frac{1-2q}{2}\mathbf1_{a_i=D(k)_i}\mathbf1_{a'_i=D(l)_i} +\frac q2\mathbf1_{a_i=a'_i}\mathbf1_{D(k)_i=D(l)_i} \right]

has no positive semidefinite matrix $R$ indexed by $(\{0,1\}^{J}\times L)\times L$ satisfying

\sum_{h\in L}R_{((a,k),h),((a',l),h)} = \sum_{h\in L}R_{((a,h),k),((a',h),l)} =[P_D(q)]_{(a,k),(a',l)}

for every $a,a',k,l$ .

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