II B: removal of constant columns preserves threshold, (8)

Open

QAlgorithms.Papers.Independent.Intakethird100.P30.constantColumns

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

prove2quantum

Let $C=(C_k)_{k\in K}$ be a nonempty code of distinct $n$ -bit words, $n\ge1$ . Separate its coordinates into the fixed coordinates $F$ and the varying coordinates $V$ . Let $D_k=C_k|_V$ , and let $\beta=C_{k_0}|_F$ for any chosen codeword $k_0$ ; the latter does not depend on the chosen word. The residual words remain distinct and have no constant coordinates. For the Bob-only filtered operators, explicit restriction of Alice's coordinate register gives

P_C(Q)=P_{\{\beta\}}(Q)\otimes P_D(Q),\qquad \mathrm{Ext}_B(P_{\{\beta\}}(Q)),\qquad Q_C^*=Q_D^* \quad(0\le Q\le\tfrac12).

The singleton factor has a one-dimensional Bob register. This retains the full factorization underlying column deletion. A singleton original code can leave a zero-length residual register, which is only a helper case and has threshold zero.

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.4, (8): deletion of every constant column, with full factorization
under coordinate restriction and the extendable one-dimensional-B factor.
The residual coordinate register may be empty for a singleton code. -/
theorem constantColumns {n : ℕ} (hn : 1 ≤ n) [Nonempty K]
    (C : K → Qubits n) (hC : Function.Injective C) (k0 : K) :
    Function.Injective (deleteConstants C) ∧ NoConstantColumns (deleteConstants C) ∧
    (∀ Q : ℝ, 0 ≤ Q → Q ≤ 1 / 2 →
      BobExtendible (bobState (fun _ : Unit => fun i : FixedCoordinates C => C k0 i.val) Q) ∧
      ∀ (a a2 : Qubits n) (k l : K),
        bobState C Q (a, k) (a2, l) =
          bobState (fun _ : Unit => fun i : FixedCoordinates C => C k0 i.val) Q
            ((fun i => a i.val), ()) ((fun i => a2 i.val), ()) *
          bobState (deleteConstants C) Q
            ((fun i => a i.val), k) ((fun i => a2 i.val), l)) ∧
    bobThreshold C = bobThreshold (deleteConstants C) := 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: removal of constant columns preserves threshold, (8)

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 choose $k_0\in K$ . Let $F=\{i:\forall k,l,\ C(k)_i=C(l)_i\}$ and $V=\{i:\exists k,l,\ C(k)_i\ne C(l)_i\}$ ; define $C_V(k)_i=C(k)_i$ for $i\in V$ , and define the one-label code $C_F(*)_i=C(k_0)_i$ for $i\in F$ . For any code $E:L\to\{0,1\}^{J}$ , put

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).

The theorem asserts that $C_V$ is injective and that every coordinate of $C_V$ takes different values on some pair of labels. For every $Q\in[0,1/2]$ , it asserts that $B_{C_F,Q}$ admits a positive semidefinite extension to two copies of its label subsystem with both corresponding partial traces equal to $B_{C_F,Q}$ , and that, for every $a,a'\in\{0,1\}^{n}$ and $k,l\in K$ ,

B_{C,Q}((a,k),(a',l)) = B_{C_F,Q}((a|_F,*),(a'|_F,*))\, B_{C_V,Q}((a|_V,k),(a'|_V,l)).

It also asserts $b(C)=b(C_V)$ , where $b(E)$ is the supremum of $\{0\}$ together with all $q\in[0,1/2]$ for which $B_{E,q}$ has no such positive semidefinite extension; no trace-one condition is imposed on extensions. Either $F$ or $V$ may be empty: the corresponding products then equal $1$ , and the assertion about variation on an empty coordinate type is vacuous.

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