Documentation

Complexity.Foundations.Combinatorics.AffineDisperser.IndependentSources

Products of Moore determinants of independent subspaces #

Let F be a finite field with 2 ^ n elements in which every proper subfield has at most 2 ^ s elements. Given 𝔽₂-subspaces Yᵢ of F of dimensions dᵢ > s and integers 2 ≤ kᵢ < dᵢ with ∑ᵢ (dᵢ - kᵢ) ≥ n + 1 - maxᵢ dᵢ, every nonzero 𝔽₂-linear functional z ↦ Tr (μ z) is nonzero on some product ∏ᵢ Δ(uᵢ) of Moore determinants of families uᵢ : Fin kᵢ → Yᵢ. This is the algebraic heart of the disperser for independent affine sources of Ben-Sasson and Kopparty [BenSassonKopparty2012, Theorem 6.1], with the hypothesis that no Yᵢ lies in a multiple of a proper subfield replaced by dᵢ > s; for a field of prime degree s = 1.

The proof follows [BSK12]. Parametrize Yᵢ by its image-subspace polynomial Qᵢ; then w ↦ Tr (μ ∏ᵢ Δ(Qᵢ ∘ wᵢ)) is a reduced polynomial function whose coefficient at ∏ᵢ ∏ₗ wᵢₗ ^ 2 ^ τᵢₗ is ∑_ρ μ ^ 2 ^ ρ ∏ᵢ per(Mᵢ[τᵢ - ρ]) ^ 2 ^ ρ, where Mᵢ[τ] = (aᵢ (τ l - m) ^ 2 ^ m). Using the zero pattern of the coefficients aᵢ (Cslib.CoeffPattern) we choose τ so that every Mᵢ[τᵢ] is triangular with nonzero diagonal while for every rotation ρ ≠ 0 some Mᵢ[τᵢ - ρ] has a zero row [BenSassonKopparty2012, Claims 6.2 and 6.3]. That coefficient is then μ ∏ᵢ per(Mᵢ[τᵢ]) ≠ 0, and a reduced polynomial with a nonzero coefficient is a nonzero function (FiniteField.eq_zero_of_forall_sum_mul_prod_pow_eq_zero).

Main results #

References #

Choosing the monomial #

theorem Cslib.AffineDisperser.exists_trace_mul_prod_det_mooreMatrix_ne_zero {F : Type u_1} [Field F] [Finite F] [Algebra (ZMod 2) F] {ι : Type u_2} [Fintype ι] {n s : ℕ} (hn : Module.finrank (ZMod 2) F = n) (hs : ∀ (K : Subfield F), K ≠ ⊤ → Nat.card ↥K ≤ 2 ^ s) (Y : ι → Submodule (ZMod 2) F) (k : ι → ℕ) (hk : ∀ (i : ι), 2 ≤ k i) (hkY : ∀ (i : ι), k i < Module.finrank (ZMod 2) ↥(Y i)) (hsY : ∀ (i : ι), s < Module.finrank (ZMod 2) ↥(Y i)) (i₀ : ι) (hsum : n < Module.finrank (ZMod 2) ↥(Y i₀) + ∑ i : ι, (Module.finrank (ZMod 2) ↥(Y i) - k i)) {μ : F} (hμ : μ ≠ 0) :
∃ (u : (i : ι) → Fin (k i) → F), (∀ (i : ι) (l : Fin (k i)), u i l ∈ Y i) ∧ (Algebra.trace (ZMod 2) F) (μ * ∏ i : ι, (mooreMatrix (u i)).det) ≠ 0

Moore products of independent sources (after [BenSassonKopparty2012, Theorem 6.1]): in a field with 2 ^ n elements whose proper subfields have at most 2 ^ s elements, let Yᵢ be subspaces of dimensions dᵢ > s, and 2 ≤ kᵢ < dᵢ with n < d_{i₀} + ∑ᵢ (dᵢ - kᵢ) for some i₀. Then for every μ ≠ 0 there are families uᵢ : Fin kᵢ → Yᵢ whose Moore determinants satisfy Tr (μ ∏ᵢ Δ(uᵢ)) ≠ 0.

By sum_cube_pow_eq_det_mooreMatrix, Δ(uᵢ) is the kᵢ-th finite difference of x ↦ x ^ (2 ^ kᵢ - 1) in the directions uᵢ. So the conclusion says that (xᵢ) ↦ Tr (μ ∏ᵢ xᵢ ^ (2 ^ kᵢ - 1)) has a nonzero mixed finite difference along the Yᵢ, the form in which the paper's theorem is used. The threshold n < maxᵢ dᵢ + ∑ᵢ (dᵢ - kᵢ) is one better than the paper's ∑ᵢ (dᵢ - kᵢ) > n - maxᵢ dᵢ + 1.