A high-rate systematic code with punctured-line recovery

The retained common-zero-block monomials are distinct reduced monomials, so their evaluation tables are independent. Choosing a basis among evaluation rows gives a systematic information set of exactly the retained cardinality. Every codeword preserves punctured-line recovery by linearity.

The information set and encoding matrices are chosen offline. No efficient uniform procedure for finding them is asserted.

structure Algebraic.MassProduction.HighRate.LineCode (K : Type u_1) (Coordinate : Type u_2) [Field K] [Finite K] [Fintype Coordinate] : Type (max u_1 u_2)

A systematic field-valued code whose symbols are recoverable from every punctured projective line through the target point.

• information : Set (Coordinate → K)

  The information positions, chosen once for the code.

• encode : (↑self.information → K) → (Coordinate → K) → K

  Encoding an arbitrary assignment to the information positions.

• systematic (message : ↑self.information → K) (index : ↑self.information) : self.encode message ↑index = message index

  Encoding preserves the assigned information symbols.

• lineRecovery (message : ↑self.information → K) (target : Coordinate → K) (direction : Projectivization K (Coordinate → K)) : self.encode message target = ∑ point ∈ puncturedLine target direction, self.encode message point

  Every nonzero projective direction supplies a recovery set.

theorem Algebraic.MassProduction.HighRate.digitDegrees_injective (Coordinate : Type u_1) (blockWidth blocks : ℕ) : Function.Injective digitDegrees

Digit matrices have distinct natural exponent vectors.

theorem Algebraic.MassProduction.HighRate.existsHighRateLineCode {K Coordinate : Type u} [Field K] [Fintype K] [CharP K 2] [Fintype Coordinate] [Nonempty Coordinate] (blockWidth blocks : ℕ) (blockPositive : 0 < blockWidth) (dimensionFits : Fintype.card Coordinate ≤ 2 ^ blockWidth) (fieldCard : Fintype.card K = 2 ^ (blockWidth * blocks)) : ∃ (code : LineCode K Coordinate), Nat.card ↑code.information = (2 ^ (blockWidth * Fintype.card Coordinate)) ^ blocks - (2 ^ (blockWidth * Fintype.card Coordinate) - 1) ^ blocks

A code with N - (A-1)^m information symbols exists over the whole N = A^m point space, where A = 2^(dimension * blockWidth).