III C: algebraic direct-sum structure of (14)

Open

QAlgorithms.Papers.Independent.Intakethird100.P30.fourWordFamily

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

prove2quantum

For a tail length $n\ge2$ , consider the explicit code of total block length $n+1$

C_{n+1}=\{0^{n+1},\ 0\,1^n,\ 1\,0^n,\ 1^{n+1}\}.

Its four words are distinct, it is closed under bitwise XOR, and

C_{n+1}=|R_1|R_n|,\qquad Q_{C_{n+1}}^*=Q_{R_n}^*.

Here the direct sum is Cartesian concatenation and the thresholds refer to Bob-only postselection of the six-state input. This identifies the algebraic structure and exact threshold of the family containing all three displayed four-word codes in equation (14). It makes no claim that this family is optimal among all four-word codes.

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.6, (14): the explicit four-word family is linear, equals R1 direct-sum Rn,
and has the Rn threshold; its total block length is n+1≥3. No optimality is claimed. -/
theorem fourWordFamily {n : ℕ} (hn : 2 ≤ n) :
    fourWordCode n = codeProduct (repetition (Fin 1)) (repetition (Fin n)) ∧
    Function.Injective (fourWordCode n) ∧ CodeLinear (fourWordCode n) ∧
    bobThreshold (fourWordCode n) = 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, III C: algebraic direct-sum structure of (14)

Read-back

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

For every natural number $n\ge2$ , let $F_n(b,c)$ be the Boolean word on a singleton coordinate together with $n$ further coordinates that equals $b$ on the singleton and $c$ on every further coordinate. The theorem asserts that $F_n$ equals the product of the two repetition codes, where repetition maps a Boolean value to the constant word on its coordinate set and the product places the two words on disjoint coordinate sets; that $F_n$ is injective; that for every two labels there exists a label whose word is their coordinatewise exclusive-or; and that $F_n$ and the length- $n$ repetition code have equal Bob thresholds. Here, for a finite code $D:L\to\{0,1\}^{J}$ , its Bob threshold means

\sup\!\left(\{0\}\cup \left\{q\in[0,\tfrac12]:\text{there is no positive semidefinite extension of }P_D(q) \text{ with both Bob marginals equal to }P_D(q)\right\}\right),

where

[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].

An extension is indexed by $(\{0,1\}^{J}\times L)\times L$ ; its two Bob marginals are obtained by summing over the extra $L$ index or over the first $L$ index, respectively. No trace normalization is part of this extension condition.

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