III D: complement extension and converse, (19)

Open

QAlgorithms.Papers.Independent.Intakethird100.P30.complementExtensionConverse

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

prove2quantum

For a nonempty code set $C\subseteq\{0,1\}^n$ , allowing $n=0$ , define

E(C)=\{0c:c\in C\}\ \cup\ \{1\overline c:c\in C\}.

The two blocks are disjoint, so $|E(C)|=2|C|$ , and $E(C)$ is closed under bitwise complementation. Conversely let $D$ be a nonempty complement-closed code of positive length $n+1$ , and construct its first-coordinate-zero tail code

C_D=\{c:0c\in D\}.

Then $C_D$ is nonempty and $D=E(C_D)$ , hence $|D|=2|C_D|$ . Fixing the existing first coordinate gives equality of unordered sets, and therefore also the source's representation up to equivalence. The tail may have length zero; no threshold comparison is asserted.

More generally, replacing the lower tail set by a coordinate permutation and fixed XOR translation of $C$ defines the source’s broader extension. The identity permutation with the all-one translation recovers $E(C)$ exactly.

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, (19): forward construction and its converse, permitting a zero-length tail.
Exact equality here fixes the existing first coordinate and forgets enumeration. -/
theorem complementExtensionConverse {n : ℕ} :
    (∀ C : Finset (Qubits n),
      twistedExtension C (Equiv.refl _) (fun _ => true) = complementExtension C) ∧
    (∀ C : Finset (Qubits n), C.Nonempty →
      (complementExtension C).card = 2 * C.card ∧ ComplementClosed (complementExtension C)) ∧
    (∀ D : Finset (Qubits (n + 1)), D.Nonempty → ComplementClosed D →
      (zeroTail D).Nonempty ∧ D = complementExtension (zeroTail D) ∧
      D.card = 2 * (zeroTail D).card) := 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: complement extension and converse, (19)

Read-back

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

For every natural number $n$ , including $0$ , the following three assertions hold, where $bw$ denotes prepending the bit $b$ to a string $w$ and $\overline w$ denotes complementing every bit of $w$ : first, for every finite set $C$ of length- $n$ Boolean strings, its twisted extension using the identity coordinate permutation and the all-true flip string equals its complement extension, namely $\{0w:w\in C\}\cup\{1\overline w:w\in C\}$ ; second, for every nonempty such $C$ , this union has cardinality $2|C|$ and contains the bitwise complement of each of its members; third, for every nonempty finite set $D$ of length- $(n+1)$ Boolean strings that contains the bitwise complement of each member, the set $C_D=\{(w_1,\ldots,w_n):w\in D,\ w_0=\mathrm{false}\}$ is nonempty and satisfies

D=\{0w:w\in C_D\}\cup\{1\overline w:w\in C_D\}, \qquad |D|=2|C_D|.

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