A high-rate line-parity code

Let K be a field of characteristic two with q = 2 ^ (h * m) elements and let ℓ ≤ 2 ^ h. Write every exponent e < q with m digits in base 2 ^ h, so that the exponents of a reduced monomial ∏ i, X i ^ e i on K ^ ℓ form a digit matrix D : Fin m → Fin ℓ → Fin (2 ^ h). The code is spanned by the monomials whose digit matrix has a zero column D j = 0: digit j of every exponent is zero. There are retainedDimension A m = A ^ m - (A - 1) ^ m of them, where A = 2 ^ (h * ℓ), out of q ^ ℓ = A ^ m points; by HighRate.retainedDimension_rate the fraction tends to one as m grows.

Each retained monomial sums to zero on every affine line (HighRate.sum_prod_digits_eq_zero). Rotating every exponent cyclically by j + 1 digits moves the zero digit to the top, so each rotated exponent is below 2 ^ (h * (m - 1)), and with ℓ ≤ 2 ^ h coordinates their total is below q - 1; the Frobenius twist HighRate.sum_prod_add_mul_pow_eq_zero applies. Removing the term at the point itself, its value is the sum over the punctured line, since -1 = 1 in characteristic two. The retained monomials are distinct and reduced, hence linearly independent (FiniteField.linearIndependent_prod_pow), so they span a line code with that many information symbols (LineCode.exists_card_info_eq_of_linearIndependent).

Every codeword restricts on each line to a function of degree at most q - 2, so these codes are subcodes of the lifted Reed–Solomon codes of [GKS13]; this is not formalized here. The information set and the extension are chosen noncomputably; no efficient procedure for finding them is claimed.

Main results

• Cslib.LineCode.HighRate.sum_prod_digits_eq_zero: line sums of the retained monomials vanish.
• Cslib.LineCode.HighRate.exists_lineCode: the high-rate line code.

References

• A. Guo, S. Kopparty, M. Sudan, New affine-invariant codes from lifting
• Adapted from MassProduction/HighRate/Code.lean, MassProduction/HighRate/DigitMonomials.lean, MassProduction/HighRate/Residue.lean and MassProduction/HighRate/LineParity.lean in S. Schlesinger, Boolean circuit mass production formalization.

theorem Cslib.LineCode.HighRate.sum_prod_digits_eq_zero {K : Type u_1} [Field K] [Fintype K] {ℓ : ℕ} [CharP K 2] {h m : ℕ} (hℓ : ℓ ≤ 2 ^ h) (hK : Fintype.card K = 2 ^ (h * m)) (D : Fin m → Fin ℓ → Fin (2 ^ h)) {j : Fin m} (hj : D j = 0) (u v : Fin ℓ → K) : ∑ x : K, ∏ i : Fin ℓ, (u i + x * v i) ^ ↑(finFunctionFinEquiv fun (k : Fin m) => D k i) = 0

Line parity of the retained monomials. Let K be a field of characteristic two with 2 ^ (h * m) elements and ℓ ≤ 2 ^ h. If the digit matrix D : Fin m → Fin ℓ → Fin (2 ^ h) has a zero column, the monomial with exponents e i = ∑ k, D k i * (2 ^ h) ^ k sums to zero on every affine line x ↦ u + x • v.

theorem Cslib.LineCode.HighRate.exists_lineCode {K : Type u_1} [Field K] [Fintype K] {ℓ : ℕ} [DecidableEq K] [CharP K 2] (h m : ℕ) (hℓ : ℓ ≤ 2 ^ h) (hK : Fintype.card K = 2 ^ (h * m)) : ∃ (C : LineCode K ℓ), C.info.card = retainedDimension (2 ^ (h * ℓ)) m

High-rate line code. Let K be a field of characteristic two with 2 ^ (h * m) elements and ℓ ≤ 2 ^ h. There is a line code on K ^ ℓ with exactly retainedDimension (2 ^ (h * ℓ)) m = 2 ^ (h * ℓ * m) - (2 ^ (h * ℓ) - 1) ^ m information symbols, out of Fintype.card K ^ ℓ = 2 ^ (h * ℓ * m) points.