An explicit affine disperser

For every input length N we fix the parameters of Ben-Sasson and Kopparty's construction explicitly. With ℓ = ⌊log₂ N⌋:

• L = ⌊ℓ / 3⌋ (Cslib.AffineDisperser.Explicit.primeBound);
• the field degree n is the product of the primes chosen greedily, in increasing order, from the primes in (L, 4 L] with product at most N / (ℓ + 1) ^ 2 (Cslib.AffineDisperser.Explicit.degreePrimes, Cslib.AffineDisperser.Explicit.fieldDegree);
• F = 𝔽_{2 ^ n} with the monomial basis in roots of the irreducible polynomials of least code of the prime degrees (Cslib.AffineDisperser.compositeBasis); each of these polynomials is found by an exhaustive search over fewer than 2 ^ (4 L + 1) ≤ 2 N ^ (4 / 3) codes;
• r = ⌊N / n⌋ blocks of n bits, read from the first r n input bits, block after block, each block in the mixed-radix order of the monomials (Cslib.AffineDisperser.explicitPos);
• t = ℓ + 1 and μ = 1.

The function Cslib.AffineDisperser.explicitDisperser N : BitString N → Bool is traceSym 1 r t on these blocks. Every prime factor of n exceeds L, so proper subfields of F have at most 2 ^ s elements, s = ⌊n / (L + 1)⌋, and the function is nonconstant on every affine subspace of BitString N of dimension greater than d(N) = N - r n + r * max (r + 1) s + r * (r + 1) + n t + ⌊n r / t⌋ (Cslib.AffineDisperser.exists_explicitDisperser_ne), so it is an affine disperser for dimension d(N) + 1 (Cslib.AffineDisperser.isAffineDisperser_explicitDisperser). Downstream, in the computability layer, the function is shown not to depend on the roots chosen for the basis (Cslib.AffineDisperser.traceSymBits_rootBasis_eq_explicitDisperser) and to be computable in polynomial time (Cslib.AffineDisperser.computableTidilyInPolyTime_explicitDisperser).

Ben-Sasson and Kopparty take n prime and reach dimension 6 N ^ (4 / 5) [BSK12]; the field then needs an irreducible polynomial of large prime degree, which exhaustive search cannot find in polynomial time. The composite degree keeps every search small at the price of the subfield term r s ≤ N / (L + 1), so our threshold is O(N / log N) (Cslib.AffineDisperser.eventually_explicitThreshold_le). This is far from the best explicit dispersers known: Li's dispersers work for dimension O(log N) [Li23].

Main definitions

• Cslib.AffineDisperser.Explicit.degreePrime: the j-th prime of the field degree on N bits.
• Cslib.AffineDisperser.Explicit.numBlocks: the number of blocks r = ⌊N / n⌋.
• Cslib.AffineDisperser.Explicit.symDegree: the degree t = ⌊log₂ N⌋ + 1 of the elementary symmetric polynomial.
• Cslib.AffineDisperser.Explicit.subfieldExp: the subfield exponent s = ⌊n / (L + 1)⌋.
• Cslib.AffineDisperser.ExplicitField: the field 𝔽_{2 ^ n} of the explicit disperser on N bits.
• Cslib.AffineDisperser.ExplicitMonomial: the monomials indexing the basis of ExplicitField N.
• Cslib.AffineDisperser.explicitBasis: the monomial basis of ExplicitField N.
• Cslib.AffineDisperser.explicitDisperser: the explicit function on N bits.
• Cslib.AffineDisperser.explicitThreshold: the dimension threshold d(N).

Main results

• Cslib.AffineDisperser.exists_explicitDisperser_ne: explicitDisperser N is nonconstant on every affine subspace of BitString N of dimension greater than explicitThreshold N.
• Cslib.AffineDisperser.isAffineDisperser_explicitDisperser: explicitDisperser N is an affine disperser for dimension explicitThreshold N + 1.

References

• E. Ben-Sasson, S. Kopparty, Affine dispersers from subspace polynomials
• X. Li, Two source extractors for asymptotically optimal entropy, and (many) more

def Cslib.AffineDisperser.Explicit.primeBound (N : ℕ) : ℕ

The prime bound L = ⌊⌊log₂ N⌋ / 3⌋: the field degree is a product of primes in (L, 4 L].

def Cslib.AffineDisperser.Explicit.degreePrimes (N : ℕ) : List ℕ

The primes whose product is the field degree on N bits: chosen greedily, in increasing order, from the primes in (L, 4 L] with product at most N / (⌊log₂ N⌋ + 1) ^ 2.

def Cslib.AffineDisperser.Explicit.degreePrime (N : ℕ) (j : Fin (degreePrimes N).length) : ℕ

The j-th prime of the field degree on N bits.

def Cslib.AffineDisperser.Explicit.fieldDegree (N : ℕ) : ℕ

The field degree n on N bits: the product of degreePrimes N.

def Cslib.AffineDisperser.Explicit.numBlocks (N : ℕ) : ℕ

The number of blocks r = ⌊N / n⌋.

def Cslib.AffineDisperser.Explicit.symDegree (N : ℕ) : ℕ

The degree t = ⌊log₂ N⌋ + 1 of the elementary symmetric polynomial.

def Cslib.AffineDisperser.Explicit.subfieldExp (N : ℕ) : ℕ

The subfield exponent s = ⌊n / (L + 1)⌋: proper subfields of 𝔽_{2 ^ n} have at most 2 ^ s elements.

theorem Cslib.AffineDisperser.Explicit.prime_of_mem_degreePrimes {N p : ℕ} (hp : p ∈ degreePrimes N) : primeBound N < p ∧ p ≤ 4 * primeBound N ∧ Nat.Prime p

Every member of degreePrimes N is a prime in (L, 4 L].

theorem Cslib.AffineDisperser.Explicit.nodup_degreePrimes (N : ℕ) : (degreePrimes N).Nodup

The primes in degreePrimes N are distinct.

theorem Cslib.AffineDisperser.Explicit.degreePrime_prime (N : ℕ) (j : Fin (degreePrimes N).length) : Nat.Prime (degreePrime N j)

Each degreePrime N j is prime.

theorem Cslib.AffineDisperser.Explicit.degreePrime_injective (N : ℕ) : Function.Injective (degreePrime N)

Distinct indices give distinct primes: degreePrime N is injective.

theorem Cslib.AffineDisperser.Explicit.fieldDegree_eq_prod (N : ℕ) : fieldDegree N = (degreePrimes N).prod

The field degree is the product of the list degreePrimes N.

theorem Cslib.AffineDisperser.Explicit.fieldDegree_ne_zero (N : ℕ) : fieldDegree N ≠ 0

The field degree is nonzero.

theorem Cslib.AffineDisperser.Explicit.numBlocks_mul_le (N : ℕ) : numBlocks N * fieldDegree N ≤ N

The r blocks of n bits fit in the input: r n ≤ N.

theorem Cslib.AffineDisperser.Explicit.lt_of_prime_dvd_fieldDegree {N q : ℕ} (hq : Nat.Prime q) (hqn : q ∣ fieldDegree N) : primeBound N < q

Every prime factor of the field degree exceeds L.

def Cslib.AffineDisperser.explicitThreshold (N : ℕ) : ℕ

The dimension threshold d(N) = N - r n + r * max (r + 1) s + r * (r + 1) + n t + ⌊n r / t⌋ of the explicit disperser on N bits.

@[reducible, inline]

abbrev Cslib.AffineDisperser.ExplicitField (N : ℕ) : Type

The field 𝔽_{2 ^ n} of the explicit disperser on N bits.

@[reducible, inline]

abbrev Cslib.AffineDisperser.ExplicitMonomial (N : ℕ) : Type

The monomials indexing the basis of ExplicitField N.

noncomputable def Cslib.AffineDisperser.explicitBasis (N : ℕ) : Module.Basis (ExplicitMonomial N) (ZMod 2) (ExplicitField N)

The monomial basis of ExplicitField N in roots of the irreducible polynomials of least code of the prime degrees.

def Cslib.AffineDisperser.explicitPos (N : ℕ) (q : Fin (Explicit.numBlocks N) × ExplicitMonomial N) : Fin N

The input position of coordinate J of block i: blocks follow each other, and coordinates within a block are numbered in the mixed-radix order of finPiFinEquiv.

theorem Cslib.AffineDisperser.explicitPos_injective (N : ℕ) : Function.Injective (explicitPos N)

Distinct coordinates are read from distinct input positions: explicitPos N is injective.

noncomputable def Cslib.AffineDisperser.explicitDisperser (N : ℕ) : BitString N → Bool

The explicit affine disperser on N bits: Ben-Sasson and Kopparty's function traceSym 1 r t on the r = numBlocks N elements of 𝔽_{2 ^ n}, n = fieldDegree N, read from the first r n input bits in the monomial basis explicitBasis N, with t = symDegree N.

theorem Cslib.AffineDisperser.exists_explicitDisperser_ne {N : ℕ} (A : AffineSubspace Bool (BitString N)) (hA : explicitThreshold N < Module.finrank Bool ↥A.direction) : ∃ x ∈ A, ∃ y ∈ A, explicitDisperser N x ≠ explicitDisperser N y

An explicit affine disperser, after [BenSassonKopparty2012, Theorem 7.3]: explicitDisperser N is nonconstant on every affine subspace of BitString N of dimension greater than explicitThreshold N.

theorem Cslib.AffineDisperser.isAffineDisperser_explicitDisperser (N : ℕ) : BitString.IsAffineDisperser (explicitDisperser N) (explicitThreshold N + 1)

The explicit function is an affine disperser for dimension explicitThreshold N + 1: it is nonconstant on the image of every injective affine map from BitString (explicitThreshold N + 1) (Cslib.BitString.IsAffineDisperser).