Affine dispersers on bit strings

Ben-Sasson and Kopparty's function traceSym reads r elements of a field F with 2 ^ n elements. On bit strings it reads them from r * n of the N input bits: element i has coordinate x (pos (i, j)) on the vector b j of an 𝔽₂-basis b of F (Cslib.AffineDisperser.readField), and the output is the trace as a bit (Cslib.AffineDisperser.traceSymBits).

Bits form the two-element field (Mathlib's BooleanRing Bool), identified with ZMod 2 by Cslib.BitString.bitEquiv, so the affine subspaces of the cube BitString N are Mathlib's AffineSubspace Bool (BitString N). Reading field elements is 𝔽₂-linear and forgets only the N - r n unread bits, so it maps an affine subspace of dimension d onto one of dimension at least d - (N - r n), and Cslib.AffineDisperser.exists_traceSym_ne transfers to bit strings (Cslib.AffineDisperser.exists_traceSymBits_ne).

Main definitions

• Cslib.AffineDisperser.readField: r field elements read from a bit string.
• Cslib.AffineDisperser.traceSymBits: traceSym on bit strings.

Main results

• Cslib.AffineDisperser.exists_traceSymBits_ne: traceSymBits is nonconstant on every affine subspace of BitString N of dimension greater than N - r n + r * max (r + 1) s + r * (r + 1) + n * t + n * r / t.

References

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

noncomputable def Cslib.AffineDisperser.readField {F : Type u_1} [Field F] [Algebra (ZMod 2) F] {ι : Type u_2} [Fintype ι] {r N : ℕ} (b : Module.Basis ι (ZMod 2) F) (pos : Fin r × ι → Fin N) (x : BitString N) : Fin r → F

The r elements of F read from the bits of x: element i has coordinate x (pos (i, j)) on the basis vector b j.

noncomputable def Cslib.AffineDisperser.traceSymBits {F : Type u_1} [Field F] [Algebra (ZMod 2) F] {ι : Type u_2} [Fintype ι] {N : ℕ} (μ : F) (r t : ℕ) (b : Module.Basis ι (ZMod 2) F) (pos : Fin r × ι → Fin N) (x : BitString N) : Bool

Ben-Sasson and Kopparty's function traceSym μ r t on bit strings: the trace, as a bit, at the r field elements read from x by readField b pos.

theorem Cslib.AffineDisperser.exists_traceSymBits_ne {F : Type u_1} [Field F] [Algebra (ZMod 2) F] {ι : Type u_2} [Fintype ι] {r N : ℕ} [Finite F] {n s t : ℕ} (hn : Module.finrank (ZMod 2) F = n) (hs : ∀ (K : Subfield F), K ≠ ⊤ → Nat.card ↥K ≤ 2 ^ s) {μ : F} (hμ : μ ≠ 0) (ht : 0 < t) (b : Module.Basis ι (ZMod 2) F) {pos : Fin r × ι → Fin N} (hpos : Function.Injective pos) (A : AffineSubspace Bool (BitString N)) (hA : N - r * n + (r * max (r + 1) s + r * (r + 1) + n * t + n * r / t) < Module.finrank Bool ↥A.direction) : ∃ x ∈ A, ∃ y ∈ A, traceSymBits μ r t b pos x ≠ traceSymBits μ r t b pos y

Affine dispersers on bit strings [BenSassonKopparty2012, Theorem 7.3]: if F has 2 ^ n elements, its proper subfields at most 2 ^ s, μ ≠ 0, 0 < t and the reading positions pos are distinct, then traceSymBits μ r t b pos is nonconstant on every affine subspace A of BitString N of dimension greater than N - r * n + (r * max (r + 1) s + r * (r + 1) + n * t + n * r / t).