Line codes spanned by line-parity functions

Line parity is a linear condition, so every linear combination of functions with line parity has line parity. If f : ι → (Fin ℓ → K) → K is linearly independent, its evaluation rows x ↦ (f i x)_i span ι → K, so some set of points has rows forming a basis of ι → K. This set is the information set: data on it is extended by applying, to the row of every point, the linear functional that takes the given values on the basis rows. The extension is a linear combination of the f i, so it inherits their line parity.

Main results

• Cslib.LineCode.exists_card_info_eq_of_linearIndependent: linearly independent functions with line parity span a line code with Fintype.card ι information symbols.

References

• Adapted from MassProduction/HighRate/Systematic.lean and MassProduction/HighRate/Code.lean in S. Schlesinger, Boolean circuit mass production formalization.

theorem Cslib.LineCode.exists_card_info_eq_of_linearIndependent {K : Type u_1} [Field K] [Fintype K] [DecidableEq K] {ℓ : ℕ} {ι : Type u_2} [Fintype ι] (f : ι → (Fin ℓ → K) → K) (hf : LinearIndependent K f) (hsum : ∀ (i : ι) (u v : Fin ℓ → K), v ≠ 0 → ∑ c ∈ Finset.univ.erase 0, f i (u + c • v) = f i u) : ∃ (C : LineCode K ℓ), C.info.card = Fintype.card ι

If f : ι → (Fin ℓ → K) → K is linearly independent and every f i has line parity, there is a line code on K ^ ℓ with exactly Fintype.card ι information symbols. (The code built in the proof is spanned by the f i; the statement records only its size.)