Subfunctions of formulas and of rectangle-free functions

The subfunctions of f on a block Y of coordinates are the functions of the coordinates in Y obtained by fixing the coordinates outside Y.

Nechiporuk's lemma bounds their number for a formula: fixing the outside coordinates turns every leaf outside Y into a constant, which then collapses the adjacent gate into one of the four unary functions of its other input. Since unary functions are closed under composition, a formula with l leaves in Y has at most 4 ^ (2 l - 1) subfunctions on Y up to unary post-composition (card_unaryClosure_subfunctions_le), hence at most 2 · 16 ^ l subfunctions.

A rectangle-free function has many subfunctions on every block: grouping the outside assignments by the subfunction they induce gives one-rectangles, so every class is small or its subfunction accepts few inputs, and the count of accepting inputs forces at least 2 ^ |Yᶜ| / (8 K) classes (two_pow_card_compl_le).

noncomputable def Algebraic.Nechiporuk.subfunctions {n : ℕ} (f : Cslib.BooleanFunction n) (Y : Finset (Fin n)) : Finset ((↥Y → Bool) → Bool)

The subfunctions of f on the block Y: fix the coordinates outside Y.

Equations

• Algebraic.Nechiporuk.subfunctions f Y = Finset.image (fun (z : ↥Yᶜ → Bool) (y : ↥Y → Bool) => f (Algebraic.Cutwidth.glue Y y z)) Finset.univ

theorem Algebraic.Nechiporuk.mem_subfunctions {n : ℕ} {f : Cslib.BooleanFunction n} {Y : Finset (Fin n)} {g : (↥Y → Bool) → Bool} : g ∈ subfunctions f Y ↔ ∃ (z : ↥Yᶜ → Bool), (fun (y : ↥Y → Bool) => f (Cutwidth.glue Y y z)) = g

theorem Algebraic.Nechiporuk.restrict_mem_subfunctions {n : ℕ} (f : Cslib.BooleanFunction n) (Y : Finset (Fin n)) (z : ↥Yᶜ → Bool) : (fun (y : ↥Y → Bool) => f (Cutwidth.glue Y y z)) ∈ subfunctions f Y

Closure under unary post-composition

noncomputable def Algebraic.Nechiporuk.unaryClosure {n : ℕ} {Y : Finset (Fin n)} (S : Finset ((↥Y → Bool) → Bool)) : Finset ((↥Y → Bool) → Bool)

Compositions of the functions in S with the four unary Boolean functions.

Equations

• Algebraic.Nechiporuk.unaryClosure S = Finset.image (fun (p : (Bool → Bool) × ((↥Y → Bool) → Bool)) => p.1 ∘ p.2) (Finset.univ ×ˢ S)

theorem Algebraic.Nechiporuk.mem_unaryClosure {n : ℕ} {Y : Finset (Fin n)} {S : Finset ((↥Y → Bool) → Bool)} {g : (↥Y → Bool) → Bool} : g ∈ unaryClosure S ↔ ∃ (u : Bool → Bool), ∃ h ∈ S, u ∘ h = g

theorem Algebraic.Nechiporuk.subset_unaryClosure {n : ℕ} {Y : Finset (Fin n)} (S : Finset ((↥Y → Bool) → Bool)) : S ⊆ unaryClosure S

theorem Algebraic.Nechiporuk.unaryClosure_mono {n : ℕ} {Y : Finset (Fin n)} {S T : Finset ((↥Y → Bool) → Bool)} (h : S ⊆ T) : unaryClosure S ⊆ unaryClosure T

theorem Algebraic.Nechiporuk.unaryClosure_unaryClosure {n : ℕ} {Y : Finset (Fin n)} (S : Finset ((↥Y → Bool) → Bool)) : unaryClosure (unaryClosure S) ⊆ unaryClosure S

Unary functions compose, so the closure is idempotent.

theorem Algebraic.Nechiporuk.card_unaryClosure_le {n : ℕ} {Y : Finset (Fin n)} (S : Finset ((↥Y → Bool) → Bool)) : (unaryClosure S).card ≤ 4 * S.card

theorem Algebraic.Nechiporuk.card_unaryClosure_le_two {n : ℕ} {Y : Finset (Fin n)} {S : Finset ((↥Y → Bool) → Bool)} (h : ∀ g ∈ S, ∃ (c : Bool), ∀ (y : ↥Y → Bool), g y = c) : (unaryClosure S).card ≤ 2

Unary compositions of constant functions are constant, so there are at most two.

Nechiporuk's counting lemma

def Algebraic.Nechiporuk.bound : ℕ → ℕ

The bound on the unary closure of the subfunctions of a formula with l leaves in the block: 2 for l = 0 and 4 ^ (2 l - 1) otherwise.

Equations

• Algebraic.Nechiporuk.bound 0 = 2
• Algebraic.Nechiporuk.bound l.succ = 4 ^ (2 * l + 1)

theorem Algebraic.Nechiporuk.bound_le (l : ℕ) : bound l ≤ 2 * 16 ^ l

theorem Algebraic.Nechiporuk.four_mul_bound_mul_bound (a b : ℕ) : 4 * bound (a + 1) * bound (b + 1) = bound (a + 1 + (b + 1))

theorem Algebraic.Nechiporuk.card_unaryClosure_subfunctions_le {n : ℕ} (Y : Finset (Fin n)) (F : Binary.Formula n) : (unaryClosure (subfunctions F.eval Y)).card ≤ bound (Binary.Formula.leavesIn Y F)

Nechiporuk's lemma: up to unary post-composition, a formula with l leaves in Y has at most bound l subfunctions on Y.

theorem Algebraic.Nechiporuk.card_subfunctions_le {n : ℕ} (Y : Finset (Fin n)) (F : Binary.Formula n) : (subfunctions F.eval Y).card ≤ 2 * 16 ^ Binary.Formula.leavesIn Y F

A formula with l leaves in Y has at most 2 · 16 ^ l subfunctions on Y.

Rectangle-free functions have many subfunctions

noncomputable def Algebraic.Nechiporuk.ones {n : ℕ} {Y : Finset (Fin n)} (g : (↥Y → Bool) → Bool) : ℕ

The number of inputs on which a function of the block is 1.

Equations

• Algebraic.Nechiporuk.ones g = {y : ↥Y → Bool | g y = true}.card

theorem Algebraic.Nechiporuk.ones_le {n : ℕ} {Y : Finset (Fin n)} (g : (↥Y → Bool) → Bool) : ones g ≤ 2 ^ Y.card

noncomputable def Algebraic.Nechiporuk.fiber {n : ℕ} (f : Cslib.BooleanFunction n) (Y : Finset (Fin n)) (g : (↥Y → Bool) → Bool) : Finset (↥Yᶜ → Bool)

The outside assignments inducing a given subfunction.

Equations

• Algebraic.Nechiporuk.fiber f Y g = {z : ↥Yᶜ → Bool | (fun (y : ↥Y → Bool) => f (Algebraic.Cutwidth.glue Y y z)) = g}

theorem Algebraic.Nechiporuk.mem_fiber {n : ℕ} {f : Cslib.BooleanFunction n} {Y : Finset (Fin n)} {g : (↥Y → Bool) → Bool} {z : ↥Yᶜ → Bool} : z ∈ fiber f Y g ↔ (fun (y : ↥Y → Bool) => f (Cutwidth.glue Y y z)) = g

theorem Algebraic.Nechiporuk.card_accepting_eq_sum {n : ℕ} (f : Cslib.BooleanFunction n) (Y : Finset (Fin n)) : (Cutwidth.accepting f).card = ∑ z : ↥Yᶜ → Bool, ones fun (y : ↥Y → Bool) => f (Cutwidth.glue Y y z)

Accepting inputs, counted fiber by fiber over the outside assignments.

theorem Algebraic.Nechiporuk.sum_ones_eq {n : ℕ} (f : Cslib.BooleanFunction n) (Y : Finset (Fin n)) : (∑ z : ↥Yᶜ → Bool, ones fun (y : ↥Y → Bool) => f (Cutwidth.glue Y y z)) = ∑ g ∈ subfunctions f Y, ones g * (fiber f Y g).card

Grouping outside assignments by the subfunction they induce.

theorem Algebraic.Nechiporuk.two_pow_card_compl_le {n : ℕ} {f : Cslib.BooleanFunction n} {K : ℕ} (hrect : Cutwidth.RectangleFree f K) (hacc : 2 ^ (n - 2) ≤ (Cutwidth.accepting f).card) {Y : Finset (Fin n)} (hY : 8 * K ≤ 2 ^ Y.card) : 2 ^ Yᶜ.card ≤ 8 * K * (subfunctions f Y).card

Rectangle-free functions have many subfunctions on every block. With 2 ^ (n - 2) accepting inputs, K-rectangle-freeness, and 2 ^ |Y| ≥ 8 K, the block Y carries at least 2 ^ |Yᶜ| / (8 K) distinct subfunctions.