Affine dispersers from subspace polynomials

Let F be a finite field with 2 ^ n elements and μ ∈ F nonzero. Ben-Sasson and Kopparty's function on r blocks [BenSassonKopparty2012, Theorem 7.3] is f(x) = Tr (μ ∑_{|I| = t} ∏_{i ∈ I} xᵢ ^ (2 ^ (r + 1 - i) - 1)), the trace of the t-th elementary symmetric polynomial of the powers xᵢ ^ (2 ^ (r + 1 - i) - 1) (blocks numbered from 0). It is nonconstant on every 𝔽₂-affine subspace A ⊆ Fʳ of large dimension.

Ben-Sasson and Kopparty take n prime, so that 𝔽₂ is the only proper subfield of F. We prove the theorem for every F whose proper subfields have at most 2 ^ s elements, replacing their threshold r + 1 on the dimensions of the useful blocks by M = max (r + 1) s: f is nonconstant on every affine A with dim A > r M + r (r + 1) + n t + ⌊n r / t⌋. Composite degrees n with no small proper divisors keep s small while allowing explicit field arithmetic.

The proof: let Yᵢ be the pivot spaces of the direction of A and lift a basis of each to vectors of A's direction vanishing below their block. Averaging gives t blocks I₀ with dᵢ > M and ∑_{I₀} (dᵢ - kᵢ) > n, kᵢ = r + 1 - i. Summing f over the cube spanned by kᵢ lifted directions in each block i ∈ I₀ expands every term ∏_{j ∈ J} xⱼ ^ (2 ^ kⱼ - 1) into covering assignments of factors to directions (Cslib.sum_cube_prod_affine). Because kᵢ decreases strictly, a weighting argument [BenSassonKopparty2012, Claim 7.4] shows that only J = I₀ survives, where block-triangularity turns the sum into ∏_{I₀} Δ(uᵢ) of Moore determinants. The independent-sources theorem (exists_trace_mul_prod_det_mooreMatrix_ne_zero) chooses the uᵢ so that its trace is nonzero, while a constant function would have zero cube sum.

Main definitions

• Cslib.AffineDisperser.traceSym: Ben-Sasson and Kopparty's symmetric-power function; Cslib.AffineDisperser.traceSym_eq_esymm writes it with Multiset.esymm.

Main results

• Cslib.AffineDisperser.eq_of_covering: the weighting argument [BenSassonKopparty2012, Claim 7.4].
• Cslib.AffineDisperser.exists_traceSym_ne: traceSym is nonconstant on affine subspaces of dimension greater than r * max (r + 1) s + r * (r + 1) + n * t + n * r / t.

References

• E. Ben-Sasson, S. Kopparty, Affine dispersers from subspace polynomials

theorem Cslib.AffineDisperser.eq_of_covering {r : ℕ} (k : Fin r → ℕ) (hk : StrictAnti k) (hk0 : ∀ (i : Fin r), 0 < k i) (I J : Finset (Fin r)) (hcard : J.card = I.card) (ℓ : (j : ↥J) × Fin (k ↑j) → Option ((i : ↥I) × Fin (k ↑i))) (hcov : ∀ (v : (i : ↥I) × Fin (k ↑i)), ∃ (p : (j : ↥J) × Fin (k ↑j)), ℓ p = some v) (hmono : ∀ (p : (j : ↥J) × Fin (k ↑j)) (v : (i : ↥I) × Fin (k ↑i)), ℓ p = some v → ↑v.fst ≤ ↑p.fst) : J = I

Covering assignments respect blocks [BenSassonKopparty2012, Claim 7.4]. Blocks i < r carry k i slots, with k strictly decreasing and positive. Let I, J be sets of t blocks and ℓ an assignment of the slots of J to the slots of I (or to nothing) that covers every slot of I and never sends a slot to a higher block. Then J = I.

noncomputable def Cslib.AffineDisperser.traceSym {F : Type u_1} [Field F] [Algebra (ZMod 2) F] (μ : F) (r t : ℕ) (x : Fin r → F) : ZMod 2

Ben-Sasson and Kopparty's symmetric-power function on r blocks of a field F [BenSassonKopparty2012, Theorem 7.3]: the trace of μ times the t-th elementary symmetric polynomial of xᵢ ^ (2 ^ (r + 1 - i) - 1), blocks numbered from 0.

theorem Cslib.AffineDisperser.traceSym_eq_esymm {F : Type u_1} [Field F] [Algebra (ZMod 2) F] (μ : F) (r t : ℕ) (x : Fin r → F) : traceSym μ r t x = (Algebra.trace (ZMod 2) F) (μ * (Multiset.map (fun (i : Fin r) => x i ^ (2 ^ (r + 1 - ↑i) - 1)) Finset.univ.val).esymm t)

traceSym is the trace of μ times the t-th elementary symmetric function (Multiset.esymm) of the powers xᵢ ^ (2 ^ (r + 1 - i) - 1).

theorem Cslib.AffineDisperser.exists_traceSym_ne {F : Type u_1} [Field F] [Finite F] [Algebra (ZMod 2) F] {n s r t : ℕ} (hn : Module.finrank (ZMod 2) F = n) (hs : ∀ (K : Subfield F), K ≠ ⊤ → Nat.card ↥K ≤ 2 ^ s) {μ : F} (hμ : μ ≠ 0) (ht : 0 < t) (A : AffineSubspace (ZMod 2) (Fin r → F)) (hA : r * max (r + 1) s + r * (r + 1) + n * t + n * r / t < Module.finrank (ZMod 2) ↥A.direction) : ∃ x ∈ A, ∃ y ∈ A, traceSym μ r t x ≠ traceSym μ r t y

Affine dispersers from subspace polynomials [BenSassonKopparty2012, Theorem 7.3], for fields whose proper subfields have at most 2 ^ s elements: if μ ≠ 0 and 0 < t, then traceSym μ r t is nonconstant on every 𝔽₂-affine subspace A of Fʳ of dimension greater than r * max (r + 1) s + r * (r + 1) + n * t + n * r / t, where F has 2 ^ n elements.

No relation between n, r and t is assumed: the summand r * (r + 1) replaces the hypothesis n * t ≥ r * (r + 1) of the paper. For prime n one may take s = 1, and the bound is then 2 r (r + 1) + n t + ⌊n r / t⌋, at most r (r + 1) above the paper's.