Systematic encoding from independent evaluation functions

Independent functions on a finite point set have an information set of the same cardinality. A basis chosen from the evaluation rows gives an encoder that is systematic on those points and preserves every linear identity satisfied by the evaluation rows.

theorem Algebraic.MassProduction.HighRate.existsSystematicEncoder {K : Type u_1} {Index : Type u_2} {Point : Type u_3} [Field K] [Fintype Index] [Fintype Point] (functions : Index → Point → K) (independent : LinearIndependent K functions) : ∃ (information : Set Point), Nat.card ↑information = Fintype.card Index ∧ ∃ (encoder : (↑information → K) → (Index → K) →ₗ[K] K), ∀ (message : ↑information → K) (index : ↑information), ((encoder message) fun (coordinate : Index) => functions coordinate ↑index) = message index

Independent evaluation functions admit a full-size information set. The encoder is a linear functional applied to the evaluation row, so every linear relation among rows is preserved.