The residue obstruction behind the high-rate code

A positive exponent below dimension * (q - 1) cannot be divisible by q - 1 if its residue modulo a divisor of q is at most modulus - dimension. A common block of zero binary digits supplies exactly this residue gap.

theorem Algebraic.MassProduction.HighRate.notDvdOfResidueGap (q dimension modulus exponent : ℕ) (modulusDivides : modulus ∣ q) (exponentPositive : 0 < exponent) (exponentSmall : exponent < dimension * (q - 1)) (residueGap : exponent % modulus + dimension ≤ modulus) : ¬q - 1 ∣ exponent

A small residue excludes every positive multiple of q - 1 below dimension * (q - 1).

def Algebraic.MassProduction.HighRate.CommonZeroBlock {Coordinate : Type u_1} (degrees : Coordinate → ℕ) (start blockWidth : ℕ) : Prop

A common zero block starts at start and contains blockWidth binary digits in every coordinate exponent.

Equations

• Algebraic.MassProduction.HighRate.CommonZeroBlock degrees start blockWidth = ∀ (coordinate : Coordinate), degrees coordinate % 2 ^ (start + blockWidth) < 2 ^ start

theorem Algebraic.MassProduction.HighRate.commonZeroBlock_iff {Coordinate : Type u_1} (degrees : Coordinate → ℕ) (start blockWidth : ℕ) : CommonZeroBlock degrees start blockWidth ↔ ∀ (coordinate : Coordinate), degrees coordinate / 2 ^ start % 2 ^ blockWidth = 0

The residue definition is equivalent to the usual quotient-and-mask test that the indicated block of binary digits is zero.

theorem Algebraic.MassProduction.HighRate.predResidueOfDvd (q modulus : ℕ) (qPositive : 0 < q) (modulusPositive : 0 < modulus) (divides : modulus ∣ q) : (q - 1) % modulus = modulus - 1

The predecessor of a positive multiple of a modulus has the last possible residue.

theorem Algebraic.MassProduction.HighRate.exponentLtCardPredOfZeroBlock (width start blockWidth exponent : ℕ) (blockPositive : 0 < blockWidth) (blockFits : start + blockWidth ≤ width) (reduced : exponent < 2 ^ width) (zeroBlock : exponent % 2 ^ (start + blockWidth) < 2 ^ start) : exponent < 2 ^ width - 1

A reduced exponent containing a nonempty zero block is strictly below q - 1, when q is a power of two covering that block.

theorem Algebraic.MassProduction.HighRate.commonZeroBlockSumResidueGap {Coordinate : Type u_1} [Fintype Coordinate] (degrees : Coordinate → ℕ) (start blockWidth : ℕ) (zeroBlock : CommonZeroBlock degrees start blockWidth) (dimensionFits : Fintype.card Coordinate ≤ 2 ^ blockWidth) : ∑ coordinate : Coordinate, degrees coordinate % 2 ^ (start + blockWidth) + Fintype.card Coordinate ≤ 2 ^ (start + blockWidth)

Summing the low residues of all coordinates leaves a gap of at least the dimension, provided the block has enough distinct bit patterns.