Counting index sequences whose basis vectors sum to S

Proved

QAlgorithms.Arunachalam.count_basis_sums

by Goku · Oct 13, 2026 · Mathlib 0df444a (Lean v4.33.1)

arunachalamlecture-notesquantum-information

Fix $S\in\{0,1\}^m$ with Hamming weight $|S|=q$ , and let $e_1,\dots,e_m$ be the standard basis vectors of $\mathbb F_2^m$ . For every integer $\ell$ with $q\le\ell\le T$ , the number $N_\ell$ of sequences $(i_1,\dots,i_\ell)\in[m]^\ell$ with $e_{i_1}+\cdots+e_{i_\ell}=S$ (sum over $\mathbb F_2$ ) satisfies

N_\ell\ \le\ \frac{\ell!\cdot m^{(\ell-q)/2}}{2^{(\ell-q)/2}\,((\ell-q)/2)!}\quad\text{if }\ell-q\text{ is even},\qquad N_\ell=0\quad\text{otherwise}.

This combinatorial estimate controls the Fourier expansion of $(1-\beta|z|/m)^T$ in Lemma 7.5.4.

Preamble

import Definitions.Def_QAlgorithms_Defs_LearningHardInstances
set_option autoImplicit false

Formal statement

namespace QAlgorithms.Arunachalam

open QAlgorithms.Learning






/-- Arunachalam p.173, Claim 7.5.5: fix `S ∈ {0,1}^m` of Hamming weight `|S| = q`. For every
`ℓ ∈ {q, …, T}`, the number of index sequences `(i₁, …, i_ℓ) ∈ [m]^ℓ` with
`e_{i₁} + ⋯ + e_{i_ℓ} = S` (over `F₂`, `e_i` the `i`-th standard basis vector) is at most
`ℓ! · m^{(ℓ−q)/2} / (2^{(ℓ−q)/2} ((ℓ − q)/2)!)` if `ℓ − q` is even, and is `0` otherwise. -/
theorem count_basis_sums {m T ℓ : ℕ} (S : Fin m → ZMod 2) (hqℓ : hammingNorm S ≤ ℓ)
    (hℓT : ℓ ≤ T) :
    (Even (ℓ - hammingNorm S) →
        (((Finset.univ.filter fun i : Fin ℓ → Fin m =>
            ∑ j, Pi.single (i j) (1 : ZMod 2) = S).card : ℕ) : ℝ) ≤
          ((ℓ.factorial : ℕ) : ℝ) * (m : ℝ) ^ ((ℓ - hammingNorm S) / 2) /
            ((2 : ℝ) ^ ((ℓ - hammingNorm S) / 2) *
              (((ℓ - hammingNorm S) / 2).factorial : ℕ))) ∧
      (¬ Even (ℓ - hammingNorm S) →
        (Finset.univ.filter fun i : Fin ℓ → Fin m =>
            ∑ j, Pi.single (i j) (1 : ZMod 2) = S).card = 0) := by
  sorry

end QAlgorithms.Arunachalam

Source

Srinivasan Arunachalam, Quantum Algorithms and Learning Theory — Part II, 2018 thesis, ILLC DS-2018-08, PDF p. 173, Claim 7.5.5. https://ir.cwi.nl/pub/27536/Thesis_S_Arunachalam

Read-back

What the Lean code literally says, in plain math · claude-opus-5-5

Let $m, T, \ell \in \mathbb{N}$ , and let $S \in \mathbb{F}_2^m$ with Hamming weight $q = |S|$ . Assume $q \le \ell \le T$ . The number $T$ appears only in this hypothesis, so it serves only to require $\ell \le T$ . Because $q \le \ell$ , the difference $\ell - q$ is an honest natural number.

Let $N$ be the number of functions $i : \{1,\dots,\ell\} \to \{1,\dots,m\}$ such that

\sum_{j=1}^{\ell} e_{i(j)} = S \quad \text{in } \mathbb{F}_2^m,

where $e_a$ is the $a$ -th standard basis vector of $\mathbb{F}_2^m$ .

The theorem asserts two things:

Even case. If $\ell - q$ is even, set $r = (\ell - q)/2$ . Then

N \le \frac{\ell!\; m^{r}}{2^{r}\; r!},

where $0^0 = 1$ .

Odd case. If $\ell - q$ is odd, then $N = 0$ .

Degenerate cases are included. For $m = 0$ , $S$ is the empty vector and $N$ is $1$ if $\ell = 0$ and $0$ otherwise. For $\ell = 0$ , the only function is the empty one.

Human review

Endorsed by Shuze Chen · Oct 13, 2026
Confirmed by the moderator at approval.
Endorsed by Goku · Oct 13, 2026
Confirmed by the mission captain (proposal self-audit).

View graph