Rectangle-free Boolean functions

A one-rectangle of f : {0,1}ⁿ → {0,1} is a product P × Q, for a split of the coordinates into U and its complement, on which f is identically 1. The function is K-rectangle-free when every one-rectangle, under every split, has a side with fewer than K elements. The lower bound applies to families that are n ^ c-rectangle-free with at least 2 ^ (n - 2) accepting inputs; this development takes that property as a hypothesis.

The support lemma two_pow_lt_or_card_accepting_lt records the only use of rectangle-freeness outside the cut-counting argument: a rectangle-free function with many accepting inputs cannot ignore many coordinates.

noncomputable def Algebraic.Cutwidth.accepting {n : ℕ} (f : Cslib.BooleanFunction n) : Finset (Fin n → Bool)

The inputs accepted by a Boolean function.

Equations

• Algebraic.Cutwidth.accepting f = {x : Fin n → Bool | f x = true}

theorem Algebraic.Cutwidth.mem_accepting {n : ℕ} {f : Cslib.BooleanFunction n} {x : Fin n → Bool} : x ∈ accepting f ↔ f x = true

def Algebraic.Cutwidth.glue {n : ℕ} (U : Finset (Fin n)) (p : ↥U → Bool) (q : ↥Uᶜ → Bool) : Fin n → Bool

Combine an assignment to the coordinates in U with one to its complement.

Equations

• Algebraic.Cutwidth.glue U p q i = if h : i ∈ U then p ⟨i, h⟩ else q ⟨i, ⋯⟩

@[simp]

theorem Algebraic.Cutwidth.glue_apply_mem {n : ℕ} (U : Finset (Fin n)) (p : ↥U → Bool) (q : ↥Uᶜ → Bool) (i : ↥U) : glue U p q ↑i = p i

@[simp]

theorem Algebraic.Cutwidth.glue_apply_compl {n : ℕ} (U : Finset (Fin n)) (p : ↥U → Bool) (q : ↥Uᶜ → Bool) (i : ↥Uᶜ) : glue U p q ↑i = q i

theorem Algebraic.Cutwidth.glue_restrict {n : ℕ} (U : Finset (Fin n)) (x : Fin n → Bool) : (glue U (fun (i : ↥U) => x ↑i) fun (i : ↥Uᶜ) => x ↑i) = x

Restricting an input to U and to its complement, then gluing, recovers it.

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

Every one-rectangle of f, under every split of the coordinates, has a side with fewer than K elements.

Equations

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

theorem Algebraic.Cutwidth.RectangleFree.one_lt {n : ℕ} {f : Cslib.BooleanFunction n} {K : ℕ} (free : RectangleFree f K) {x : Fin n → Bool} (accepted : f x = true) : 1 < K

A nonzero rectangle-free function has threshold at least two.

theorem Algebraic.Cutwidth.two_pow_lt_or_card_accepting_lt {n : ℕ} {f : Cslib.BooleanFunction n} {K : ℕ} (free : RectangleFree f K) {R U : Finset (Fin n)} (depends : DependsOnlyOn f R) (disjoint : Disjoint U R) : 2 ^ U.card < K ∨ (accepting f).card < 2 ^ U.card * K

A rectangle-free function that ignores the coordinates in U either has 2 ^ |U| < K, or fewer than 2 ^ |U| * K accepting inputs.