II B: finite counts of inequivalent codes, Table I

Open

QAlgorithms.Papers.Independent.Intakethird100.P30.tableI

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

prove2quantum

For positive integers $n,m$ , let $N(n,m)$ count equivalence classes of unordered sets of $m$ distinct binary words of length $n$ with no constant columns. Equivalence permits any coordinate permutation followed by XOR with one fixed word. The exact numeric entries of Table I are

\begin{array}{c|c|l} n&m&N(n,m)\text{ in increasing order of }m\\\hline 2&2,3&1,1\\ 3&2,\ldots,7&1,2,5,3,3,1\\ 4&2,\ldots,15&1,3,13,24,47,55,73,56,50,27,19,6,4,1\\ 5&2,\ldots,6&1,4,28,104,422\\ 6&2,3,4&1,6,56\\ 7&2,3&1,7\\ 8&2,3&1,9 \end{array}

These are finite combinatorial cardinalities. No value is claimed for a dotted or shaded cell. The count uses complete group-action orbits of code sets, thereby forgetting word enumeration as well as coordinate symmetries.

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, Table I: exact finite combinatorial counts, not SDP estimates.
Dots and shaded cells do not occur in tableEntries. -/
theorem tableI : ∀ e ∈ tableEntries, codeClassCount e.1 e.2.1 = e.2.2 := 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: finite counts of inequivalent codes, Table I

Read-back

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

Let $N(n,m)$ be the number of distinct orbit sets obtained from all $m$ -element subsets $C\subseteq\{0,1\}^n$ for which every coordinate takes both Boolean values among the words of $C$ , where the orbit set of $C$ consists of all sets $\{(w_{p(i)}\oplus t_i)_i:w\in C\}$ as $p$ ranges over coordinate permutations and $t$ over all $n$ -bit words, with $\oplus$ denoting Boolean exclusive-or. The theorem asserts $N(n,m)=r$ for every triple $(n,m,r)$ in the following list:

\begin{aligned} [&(2,2,1),(2,3,1),\\ &(3,2,1),(3,3,2),(3,4,5),(3,5,3),(3,6,3),(3,7,1),\\ &(4,2,1),(4,3,3),(4,4,13),(4,5,24),(4,6,47),(4,7,55),\\ &(4,8,73),(4,9,56),(4,10,50),(4,11,27),(4,12,19),\\ &(4,13,6),(4,14,4),(4,15,1),\\ &(5,2,1),(5,3,4),(5,4,28),(5,5,104),(5,6,422),\\ &(6,2,1),(6,3,6),(6,4,56),\\ &(7,2,1),(7,3,7),(8,2,1),(8,3,9)]. \end{aligned}

It makes no assertion about pairs $(n,m)$ absent from this list.

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