Cover's enumerative coding for weight-bounded Boolean words

Cover's lexicographic rank (Cslib.BitString.coverRank) and greedy threshold decoder (Cslib.BitString.coverDecode) establish an explicit bijection between words z : Fin q → Bool of Hamming weight at most e and indices below the Hamming-ball size B(q, e) = ∑ j ∈ range (e + 1), q.choose j (Cslib.BitString.ballSize).

Main definitions

• Cslib.BitString.coverRank: Cover's lexicographic rank of a weight-bounded Boolean word.
• Cslib.BitString.coverDecode: Cover's greedy threshold decoder recovering a word of weight at most e from its rank below ballSize q e.

Main results

• Cslib.BitString.coverRank_lt_ballSize, Cslib.BitString.weight_coverDecode_le, Cslib.BitString.coverRank_coverDecode, Cslib.BitString.coverDecode_coverRank: mutual inverse and weight bounds for Cover's enumerative coding.

References

• T. M. Cover, Enumerative source encoding
• [Threshold Circuits as Decision Trees and Finite-State Programs, Section 4] [26]

def Cslib.BitString.coverRank {q : ℕ} : ℕ → (Fin q → Bool) → ℕ

Cover's lexicographic rank of a word z : Fin q → Bool among words of weight at most e.

def Cslib.BitString.coverDecode (q e t : ℕ) : Fin q → Bool

Cover's greedy threshold decoder recovering a word z : Fin q → Bool of weight at most e from its rank t < ballSize q e.

theorem Cslib.BitString.coverRank_lt_ballSize {q : ℕ} (e : ℕ) (z : Fin q → Bool) (hz : weight z ≤ e) : coverRank e z < ballSize q e

Every word z : Fin q → Bool of weight at most e has coverRank e z < ballSize q e.

theorem Cslib.BitString.weight_coverDecode_le (q e t : ℕ) : weight (coverDecode q e t) ≤ e

Every decoded word coverDecode q e t has Hamming weight at most e.

@[simp]

theorem Cslib.BitString.coverRank_coverDecode {q e t : ℕ} (ht : t < ballSize q e) : coverRank e (coverDecode q e t) = t

Ranking a decoded word coverDecode q e t for t < ballSize q e recovers t.

@[simp]

theorem Cslib.BitString.coverDecode_coverRank {q e : ℕ} (z : Fin q → Bool) (hz : weight z ≤ e) : coverDecode q e (coverRank e z) = z

Decoding the rank coverRank e z of a word z : Fin q → Bool with weight z ≤ e recovers z.