Balanced padding of a sumset disperser

One fresh input bit balances a Boolean function exactly. Two-sided sumset dispersion survives with twice the source-size threshold, so any fixed extraction error below one half suffices for the circuit lower bound's density requirement after padding.

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

Every sufficiently large pair of flat sources has both Boolean outputs among its sums. Unlike extraction, this imposes no quantitative bias bound.

Equations

• Algebraic.Cutwidth.FlatSumsetDisperser f K = ∀ (P Q : Finset (Fin n → Bool)), K ≤ P.card → K ≤ Q.card → ∀ (b : Bool), ∃ x ∈ P, ∃ y ∈ Q, f (Algebraic.Cutwidth.xorInput x y) = b

def Algebraic.Cutwidth.balancePad {n : ℕ} (f : Cslib.BooleanFunction n) : Cslib.BooleanFunction (n + 1)

XOR the original verdict with a fresh first input bit.

Equations

• Algebraic.Cutwidth.balancePad f x = (f (Fin.tail x) ^^ x 0)

def Algebraic.Cutwidth.balancePadEval (eval : List Bool → List Bool) (x : List Bool) : List Bool

The uniform list evaluator for balanced padding. The original evaluator reads the tail, and its first output bit is XORed with the first input bit.

Equations

• Algebraic.Cutwidth.balancePadEval eval x = [(eval x.tail).headD false ^^ x.headD false]