Flat-source sumset extraction

FlatSumsetExtractor f K ν is the finite-counting form of one-bit sumset extraction for two independent uniform sources, each supported on at least K inputs. It counts source pairs rather than distinct XORs, retaining the multiplicity of every output. In entropy notation the threshold is log₂ K.

This is the part of the usual sumset-extractor contract needed by the circuit lower bound. Xin Li's Two Source Extractors for Asymptotically Optimal Entropy, and (Many) More, Theorem 7.13 (2023), supplies the intended explicit construction with polynomial K. Its construction is not proved in this module. Eshan Chattopadhyay and Jyun-Jie Liao's Extractors for Sum of Two Sources (2021) supplies a sufficient subexponential threshold for the generalized circuit theorem with sublinear source entropy.

def Algebraic.Cutwidth.xorInput {n : ℕ} (x y : Fin n → Bool) : Fin n → Bool

Coordinatewise addition over the two-element field.

Equations

• Algebraic.Cutwidth.xorInput x y i = (x i ^^ y i)

noncomputable def Algebraic.Cutwidth.sumsetOnes {n : ℕ} (f : Cslib.BooleanFunction n) (P Q : Finset (Fin n → Bool)) : Finset ((Fin n → Bool) × (Fin n → Bool))

Source pairs whose sum is accepted. Repeated sums are counted separately.

Equations

• Algebraic.Cutwidth.sumsetOnes f P Q = {xy ∈ P ×ˢ Q | f (Algebraic.Cutwidth.xorInput xy.1 xy.2) = true}

def Algebraic.Cutwidth.FlatSumsetExtractor {n : ℕ} (f : Cslib.BooleanFunction n) (K : ℕ) (ν : ℝ) : Prop

One-bit sumset extraction from two independent uniform sources, with support size at least K and statistical error at most ν.

Equations

• One or more equations did not get rendered due to their size.