Enumeration by bounded weight: shrinking the search space from $2^n$ to $\sum_{k\le w}\binom nk$

(scaling, and the size of the certificate)

A lower-bound certificate can be built from a full-space enumeration (Finset.univ : Finset (Vec n)): coverage then comes for free from Finset.mem_univ, but the cost is $2^n$. In measurements $n \le 9$ runs in seconds while $n = 15$ takes over three minutes, so that route stalls around $n \approx 12$.

This module takes a different route: enumerate only the vectors of weight $\le w$. A lower bound only has to exclude operators of weight $< d$, so $w = d - 1$ suffices, and

• the candidate space drops from $2^n$ to $\sum_{k \le w}\binom nk$ (for fixed $d$, a polynomial of degree $d-1$ in $n$)
• for $n = 15$ and $d = 3$: $2^{15} = 32768 \to \binom{15}{\le 2} = 121$ (a factor of 270).

The price is that coverage of the enumeration is no longer free: the main theorem of this module, mem_lightVecs, is exactly that coverage lemma, and length_lightVecs gives the exact count. Together they state the complexity characterisation, namely that the reduced size of a distance-decision certificate is exactly $\sum_{k<d}\binom nk$.

Construction

The enumeration and the weight are defined by the same recursion, so coverage can be proved by structural induction:

wtRec : the last coordinate counts 1 when nonzero and 0 when zero, recursing on the prefix
lightVecs (n+1) (w+1) = (lightVecs n (w+1)).map (pad a zero at the last position)
                      ++ (lightVecs n w).map (pad a one at the last position)

lightVecs is exact and without repetition: its length is $\sum_{k\le w}\binom nk$.

Main results

• mem_lightVecs: coverage; every vector of weight $\le w$ occurs in the enumeration.
• wtRec_eq_hammingNorm: wtRec agrees with the standard hammingNorm (the bridge to the public interface).
• length_lightVecs: the exact count; the length of the enumeration is $\sum_{k \le w}\binom nk$.

Padding the last coordinate

def QECCertificates.snocV {n : ℕ} (u : Vec n) (b : ZMod 2) : Vec (n + 1)

"Pad the last coordinate": the first n coordinates take u and the n+1-st takes b.

Deliberately written as an explicit if branch rather than Fin.snoc, for the same reason as Fin.append: an if branch reduces coordinate by coordinate in the kernel, so by decide can compute with it.

Equations

• QECCertificates.snocV u b i = if h : ↑i < n then u ⟨↑i, h⟩ else b

@[simp]

theorem QECCertificates.snocV_castSucc {n : ℕ} {u : Vec n} {b : ZMod 2} (i : Fin n) : snocV u b i.castSucc = u i

@[simp]

theorem QECCertificates.castSuccEmb_apply {n : ℕ} (i : Fin n) : Fin.castSuccEmb i = i.castSucc

@[simp]

theorem QECCertificates.snocV_last {n : ℕ} {u : Vec n} {b : ZMod 2} : snocV u b (Fin.last n) = b

@[simp]

theorem QECCertificates.snocV_zero_zero {n : ℕ} : snocV 0 0 = 0

A zero vector padded with a zero at the last position is still the zero vector.

theorem QECCertificates.snocV_prefix_last {n : ℕ} (v : Vec (n + 1)) : snocV (fun (i : Fin n) => v i.castSucc) (v (Fin.last n)) = v

Every vector of n+1 coordinates is reconstructed from its prefix and its last coordinate.

Recursive weight and enumeration

def QECCertificates.wtRec (n : ℕ) : Vec n → ℕ

Recursive weight: a definition isomorphic to lightVecs, so that the coverage proof can proceed by structural induction.

The last coordinate counts 1 when nonzero and 0 when zero, with recursion on the prefix this agrees with hammingNorm (wtRec_eq_hammingNorm).

Equations

• QECCertificates.wtRec 0 x_2 = 0
• QECCertificates.wtRec n.succ v = (QECCertificates.wtRec n fun (i : Fin n) => v i.castSucc) + if v (Fin.last n) = 0 then 0 else 1

@[simp]

theorem QECCertificates.wtRec_zero (v : Vec 0) : wtRec 0 v = 0

theorem QECCertificates.wtRec_succ {n : ℕ} (v : Vec (n + 1)) : wtRec (n + 1) v = (wtRec n fun (i : Fin n) => v i.castSucc) + if v (Fin.last n) = 0 then 0 else 1

def QECCertificates.lightVecs (n w : ℕ) : List (Vec n)

All vectors of weight $\le w$ (a computable enumeration, exact and without repetition).

Recursion: the vectors of $n+1$ coordinates split into two classes according to their last coordinate. Those whose last coordinate is zero come from padding the vectors of $n$ coordinates of weight $\le w+1$ with a zero, and those whose last coordinate is 1 come from padding the vectors of $n$ coordinates of weight $\le w$ with a one.

Equations

• One or more equations did not get rendered due to their size.
• QECCertificates.lightVecs 0 x✝ = [0]
• QECCertificates.lightVecs n.succ 0 = [0]

@[simp]

theorem QECCertificates.lightVecs_nil (w : ℕ) : lightVecs 0 w = [0]

theorem QECCertificates.lightVecs_zero (n : ℕ) : lightVecs n 0 = [0]

theorem QECCertificates.lightVecs_succ_succ (n w : ℕ) : lightVecs (n + 1) (w + 1) = List.map (fun (u : Vec n) => snocV u 0) (lightVecs n (w + 1)) ++ List.map (fun (u : Vec n) => snocV u 1) (lightVecs n w)

Weight zero means the zero vector

theorem QECCertificates.wtRec_eq_zero_iff {n : ℕ} (v : Vec n) : wtRec n v = 0 ↔ v = 0

Coverage

theorem QECCertificates.mem_lightVecs (n w : ℕ) (v : Vec n) : wtRec n v ≤ w → v ∈ lightVecs n w

Coverage: every vector of weight $\le w$ occurs in lightVecs n w.

The proof follows the recursive structure of lightVecs by looking at the last coordinate. If the last coordinate is nonzero then the weight of the prefix must be $\le w$; if it is zero then the prefix need only have weight $\le w+1$. Each case lands in the corresponding half of the enumeration.

Bridge to the standard weight

theorem QECCertificates.wt_le_of_mem_lightVecs (n w : ℕ) (v : Vec n) : v ∈ lightVecs n w → wtRec n v ≤ w

Soundness: lightVecs contains only vectors of weight $\le w$, the other half of the coverage statement mem_lightVecs.

With both halves, the claim that the candidate set is empty is closed in both directions: coverage says nothing is missed, soundness says everything that is left really is light.

theorem QECCertificates.wtRec_eq_card_support {n : ℕ} (v : Vec n) : wtRec n v = (support v).card

wtRec is the size of the support (agreeing with support and hammingNorm).

theorem QECCertificates.wtRec_eq_hammingNorm {n : ℕ} (v : Vec n) : wtRec n v = hammingNorm v

wtRec agrees with the standard hammingNorm (the bridge to the public interface).

The exact count (size of the certificate)

theorem QECCertificates.length_lightVecs (n w : ℕ) : (lightVecs n w).length = ∑ k ∈ Finset.range (w + 1), n.choose k

The exact length of the enumeration: lightVecs n w has exactly $\sum_{k \le w}\binom nk$ elements.

This is the concrete content of the size of a distance-decision certificate: since a lower bound only has to exclude operators of weight $< d$, taking $w = d-1$ makes the candidate space exactly $\sum_{k<d}\binom nk$, a polynomial of degree $d-1$ in $n$ rather than the $2^n$ of the full space.