Rectangle freeness for both output values

Coordinatewise Boolean bijections preserve rectangles and their side sizes. Flipping the fresh bit of balanced padding negates the output, so the fixed balanced hard family has the same rectangle threshold for both output values. Its stronger sumset dispersion contract also bounds every monochromatic coset of an XOR-closed set.

theorem Algebraic.Cutwidth.RectangleFree.coordinateEquiv {n K : ℕ} {f : Cslib.BooleanFunction n} (free : RectangleFree f K) (e : Fin n → Equiv.Perm Bool) : RectangleFree (fun (x : Cslib.BitString n) => f fun (i : Fin n) => (e i) (x i)) K

Changing each input coordinate by a bijection preserves rectangle freeness.

theorem Algebraic.Cutwidth.RectangleFree.not_balancePad {n K : ℕ} {f : Cslib.BooleanFunction n} (free : RectangleFree (balancePad f) K) : RectangleFree (fun (x : Cslib.BitString (n + 1)) => !balancePad f x) K

Negating balanced padding is just a flip of its fresh input coordinate.

theorem Algebraic.Cutwidth.FlatSumsetDisperser.card_lt_of_monochromatic_coset {n K : ℕ} {f : Cslib.BooleanFunction n} (disperse : FlatSumsetDisperser f K) (V : Finset (Fin n → Bool)) (closed : ∀ x ∈ V, ∀ y ∈ V, xorInput x y ∈ V) (a : Fin n → Bool) (b : Bool) (mono : ∀ x ∈ V, f (xorInput a x) = b) : V.card < K

A sumset disperser has no large monochromatic coset of an XOR-closed set. In particular this applies to every affine subspace of the Boolean cube.

theorem Algebraic.Cutwidth.Aggregate.family_eventually_sumsetDisperser : ∀ᶠ (n : ℕ) in Filter.atTop, FlatSumsetDisperser (Extractor.sourceReductionHardFamily n) (familyThreshold n)

The balanced hard family retains two-sided sumset dispersion, which is stronger than the exclusion of monochromatic coordinate rectangles.

theorem Algebraic.Cutwidth.Aggregate.family_eventually_rectangleFree_both : ∀ᶠ (n : ℕ) in Filter.atTop, RectangleFree (Extractor.sourceReductionHardFamily n) (familyThreshold n) ∧ RectangleFree (fun (x : Cslib.BitString n) => !Extractor.sourceReductionHardFamily n x) (familyThreshold n)

The fixed polynomial-time family eventually excludes large rectangles of either constant output value, at the same threshold.