Documentation

Complexity.Foundations.Data.Code.Justesen

Justesen codes #

Let F be a finite field whose elements are written as b bits through an additive bijection φ : F ≃+ BitString b, so that F has q = 2 ^ b elements; every field of characteristic two with 2 ^ b elements has such a bijection (Cslib.nonempty_addEquiv_bitString). The Justesen code [Jus72], [GRS19] of outer dimension K concatenates the Reed–Solomon code of dimension K whose evaluation points are the q - 1 nonzero elements u of F with inner codes that vary with the position: the symbol a at the position u becomes the 2 * b bits of (a, u * a), its Wozencraft encoding Cslib.Code.wozencraft (Cslib.Code.justesen, Cslib.Code.justesenCode). No search over inner codes is involved, which is what makes the construction explicit.

Nonzero symbols at distinct positions have distinct Wozencraft encodings, since (a, u * a) determines a and then u (Cslib.Code.wozencraft_inj). Two distinct Reed–Solomon codewords differ at s ≥ q - K positions; the differences of their inner blocks there are s distinct nonzero binary words of length 2 * b, at most V(r) = ∑_{j ≤ r} C(2 * b, j) of which have weight at most r (Cslib.BitString.card_filter_weight_le). So their Justesen encodings are at distance at least (q - K - V(r)) * (r + 1) for every r (Cslib.Code.le_minDist_justesenCode), by the counting bound Cslib.Code.sub_card_mul_le_sum_hammingNorm.

With the binomial estimate V(r) * 4 ^ (2 * b) ≤ 4 ^ r * 5 ^ (2 * b) (Cslib.Code.sum_range_choose_mul_four_pow_le), this shows that Justesen codes are asymptotically good (Cslib.Code.IsAsymptoticallyGood): for b = 16 * s and K = 2 ^ (16 * s - 1), the Justesen code is a binary code of length n = 32 * s * (2 ^ (16 * s) - 1) with 2 ^ k codewords, where n ≤ 4 * k, and minimum distance at least n / 128 (Cslib.Code.card_le_mul_minDist_justesenCode, Cslib.Code.isAsymptoticallyGood_justesenCode); the lengths grow without bound with s, while the rate stays at least 1 / 4 and the relative distance at least 1 / 128. These constants are not optimized: estimating V(r) by the binary entropy function H instead gives relative distance approaching (1 - 2 R) H⁻¹(1 / 2) ≈ 0.11 * (1 - 2 R) at rate R < 1 / 2 [GRS19]; this is not formalized here.

Main definitions #

Main results #

References #

Weights of distinct words #

source
theorem Cslib.Code.sub_card_mul_le_sum_hammingNorm {σ : Type u_1} {κ : Type u_2} {β : Type u_3} [Fintype κ] [DecidableEq κ] [Fintype β] [DecidableEq β] [Zero β] {S : Finset σ} {g : σ → κ → β} (hg : Set.InjOn g ↑S) (r : ℕ) :
(S.card - {x : κ → β | hammingNorm x ≤ r}.card) * (r + 1) ≤ ∑ u ∈ S, hammingNorm (g u)

Distinct words are heavy. If g is injective on S, the words g u for u ∈ S have total weight at least (#S - V) * (r + 1), where V is the number of words of weight at most r.

source
theorem Cslib.Code.sum_range_choose_mul_four_pow_le (ℓ r : ℕ) :
(∑ j ∈ Finset.range (r + 1), ℓ.choose j) * 4 ^ ℓ ≤ 4 ^ r * 5 ^ ℓ

A binomial estimate for the size of a Hamming ball: V * 4 ^ ℓ ≤ 4 ^ r * 5 ^ ℓ for V = ∑_{j ≤ r} C(ℓ, j), since 5 ^ ℓ = ∑_j C(ℓ, j) * 4 ^ (ℓ - j).

The Wozencraft encoding #

source
def Cslib.Code.wozencraft {F : Type u_1} [Field F] {b : ℕ} (φ : F ≃+ BitString b) (u a : F) :
Fin 2 × Fin b → Bool

The Wozencraft encoding of the symbol a with multiplier u: the binary word on Fin 2 × Fin b holding the bits of a in its first half and the bits of u * a in its second, read through the additive bijection φ : F ≃+ BitString b.

Instances For
    source
    theorem Cslib.Code.wozencraft_sub {F : Type u_1} [Field F] {b : ℕ} (φ : F ≃+ BitString b) (u a a' : F) :
    wozencraft φ u (a - a') = wozencraft φ u a - wozencraft φ u a'

    The Wozencraft encoding with a fixed multiplier is additive.

    source
    theorem Cslib.Code.wozencraft_injective {F : Type u_1} [Field F] {b : ℕ} (φ : F ≃+ BitString b) (u : F) :
    Function.Injective (wozencraft φ u)

    The Wozencraft encoding with a fixed multiplier is injective: the first half of the encoding holds the bits of the symbol.

    source
    theorem Cslib.Code.wozencraft_inj {F : Type u_1} [Field F] {b : ℕ} (φ : F ≃+ BitString b) {u u' a a' : F} (ha : a ≠ 0) (h : wozencraft φ u a = wozencraft φ u' a') :
    u = u' ∧ a = a'

    Distinct inner codes. The Wozencraft encoding of a nonzero symbol determines the symbol and the multiplier: nonzero symbols at distinct positions of a Justesen codeword have distinct encodings.

    Justesen codes #

    source
    def Cslib.Code.justesen {F : Type u_1} [Field F] {b : ℕ} (φ : F ≃+ BitString b) (c : Fˣ → F) :
    Fˣ × Fin 2 × Fin b → Bool

    The Justesen encoding of an outer word c on the nonzero elements of F: the concatenation whose block at the position u is the Wozencraft encoding of c u with multiplier u.

    Instances For
      source
      theorem Cslib.Code.justesen_injective {F : Type u_1} [Field F] {b : ℕ} (φ : F ≃+ BitString b) :
      Function.Injective (justesen φ)

      The Justesen encoding is injective.

      source
      noncomputable def Cslib.Code.justesenCode {F : Type u_1} [Field F] {b : ℕ} (φ : F ≃+ BitString b) (K : ℕ) :
      Set (Fˣ × Fin 2 × Fin b → Bool)

      The Justesen code of outer dimension K: the Justesen encodings of the codewords of the Reed–Solomon code of dimension K whose evaluation points are the nonzero elements of F.

      Instances For
        source
        theorem Cslib.Code.le_minDist_justesenCode {F : Type u_1} [Field F] {b : ℕ} [Fintype F] [DecidableEq F] (φ : F ≃+ BitString b) (K r : ℕ) :
        ↑((Fintype.card F - K - ∑ j ∈ Finset.range (r + 1), (2 * b).choose j) * (r + 1)) ≤ minDist (justesenCode φ K)

        The distance of Justesen codes [Jus72]. For a field with q elements written as b bits, the Justesen code of outer dimension K has minimum distance at least (q - K - V(r)) * (r + 1) for every r, where V(r) = ∑_{j ≤ r} C(2 * b, j) is the number of binary words of length 2 * b and weight at most r.

        source
        theorem Cslib.Code.card_justesenCode {F : Type u_1} [Field F] {b : ℕ} [Fintype F] (φ : F ≃+ BitString b) {K : ℕ} (hK : K ≤ Fintype.card F - 1) :
        Nat.card ↑(justesenCode φ K) = 2 ^ (b * K)

        The number of Justesen codewords. For a field with q elements written as b bits and K ≤ q - 1, the Justesen code of outer dimension K has q ^ K = 2 ^ (b * K) codewords.

        source
        theorem Cslib.Code.card_le_mul_minDist_justesenCode {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] {s : ℕ} (hs : 1 ≤ s) (φ : F ≃+ BitString (16 * s)) :
        ↑(Fintype.card (Fˣ × Fin 2 × Fin (16 * s))) ≤ 128 * minDist (justesenCode φ (2 ^ (16 * s - 1)))

        The relative distance of Justesen codes at rate at least 1 / 4 [Jus72]. Let s ≥ 1 and let F be a field written as b = 16 * s bits, which then has 2 ^ (16 * s) elements. The Justesen code of outer dimension K = 2 ^ (16 * s - 1) is a binary code of length n = 32 * s * (2 ^ (16 * s) - 1) whose minimum distance d satisfies n ≤ 128 * d.

        source
        theorem Cslib.Code.isAsymptoticallyGood_justesenCode {F : ℕ → Type u_2} [(s : ℕ) → Field (F s)] [(s : ℕ) → Fintype (F s)] [(s : ℕ) → DecidableEq (F s)] (φ : (s : ℕ) → F s ≃+ BitString (16 * (s + 1))) :
        IsAsymptoticallyGood fun (s : ℕ) => justesenCode (φ s) (2 ^ (16 * (s + 1) - 1))

        Justesen codes are asymptotically good [Jus72]. Given for each s a field F s written as 16 * (s + 1) bits through φ s : F s ≃+ BitString (16 * (s + 1)), the Justesen codes justesenCode (φ s) (2 ^ (16 * (s + 1) - 1)) form an asymptotically good family of binary codes: their lengths 32 * (s + 1) * (2 ^ (16 * (s + 1)) - 1) grow without bound, with rate at least 1 / 4 and relative distance at least 1 / 128.