Nechiporuk's formula lower bound for rectangle-free functions

Nechiporuk's method bounds the leaf size of a formula from below by the number of distinct subfunctions on the blocks of a partition of the inputs. A rectangle-free function with many accepting inputs has nearly the maximal number of subfunctions on every block whose size exceeds log₂ (8 K) (Nechiporuk.two_pow_card_compl_le), while a formula with l leaves in a block has at most 2 · 16 ^ l subfunctions there (Nechiporuk.card_subfunctions_le). Summing over n / b disjoint blocks of size b gives leaf size Ω(n² / b); with a polynomial threshold K ≤ n ^ c the blocks have logarithmic size, and every formula over the full binary basis computing the function has Ω(n² / log n) leaves.

The main statements are sum_le_of_computes for an arbitrary family of disjoint blocks, leaves_lower_bound for consecutive blocks of a given size, and the asymptotic eventually_sq_le_leaves.

theorem Algebraic.Nechiporuk.block_bound {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) (F : Binary.Formula n) (hF : F.Computes f) : n - Y.card ≤ Nat.log 2 (16 * K) + 4 * Binary.Formula.leavesIn Y F

On a block of size at least log₂ (8 K), a formula computing a rectangle-free function with many accepting inputs has at least (n - |Y| - log₂ (16 K)) / 4 leaves in the block.

theorem Algebraic.Nechiporuk.sum_le_of_computes {n : ℕ} {f : Cslib.BooleanFunction n} {K : ℕ} (hrect : Cutwidth.RectangleFree f K) (hacc : 2 ^ (n - 2) ≤ (Cutwidth.accepting f).card) {k : ℕ} (Y : Fin k → Finset (Fin n)) (disjoint : Pairwise fun (i j : Fin k) => Disjoint (Y i) (Y j)) (hY : ∀ (i : Fin k), 8 * K ≤ 2 ^ (Y i).card) (F : Binary.Formula n) (hF : F.Computes f) : ∑ i : Fin k, (n - (Y i).card) ≤ k * Nat.log 2 (16 * K) + 4 * F.leaves

Nechiporuk's bound for rectangle-free functions. Over k pairwise disjoint blocks, each of size at least log₂ (8 K), every formula computing a K-rectangle-free function with at least 2 ^ (n - 2) accepting inputs has leaf size at least (Σ_i (n - |Y_i|) - k · log₂ (16 K)) / 4.

Consecutive blocks of a fixed size

def Algebraic.Nechiporuk.block (n b : ℕ) (i : Fin (n / b)) : Finset (Fin n)

The i-th block of b consecutive coordinates, for i < n / b.

Equations

• Algebraic.Nechiporuk.block n b i = Finset.image (fun (j : Fin b) => ⟨b * ↑i + ↑j, ⋯⟩) Finset.univ

theorem Algebraic.Nechiporuk.card_block {n b : ℕ} (i : Fin (n / b)) : (block n b i).card = b

theorem Algebraic.Nechiporuk.block_disjoint {n b : ℕ} (hb : 0 < b) : Pairwise fun (i j : Fin (n / b)) => Disjoint (block n b i) (block n b j)

theorem Algebraic.Nechiporuk.leaves_lower_bound {n : ℕ} {f : Cslib.BooleanFunction n} {K b : ℕ} (hrect : Cutwidth.RectangleFree f K) (hacc : 2 ^ (n - 2) ≤ (Cutwidth.accepting f).card) (hb : 0 < b) (hK : 8 * K ≤ 2 ^ b) (F : Binary.Formula n) (hF : F.Computes f) : n / b * (n - b) ≤ n / b * Nat.log 2 (16 * K) + 4 * F.leaves

Nechiporuk's bound with consecutive blocks of size b. With 8 K ≤ 2 ^ b, every formula computing a K-rectangle-free function with at least 2 ^ (n - 2) accepting inputs satisfies (n / b) · (n - b) ≤ (n / b) · log₂ (16 K) + 4 · leaves.

theorem Algebraic.Nechiporuk.leaves_lower_bound' {n : ℕ} {f : Cslib.BooleanFunction n} {K b : ℕ} (hrect : Cutwidth.RectangleFree f K) (hacc : 2 ^ (n - 2) ≤ (Cutwidth.accepting f).card) (hb : 0 < b) (hK : 8 * K ≤ 2 ^ b) (F : Binary.Formula n) (hF : F.Computes f) : (n - b) * (n - 2 * b - 1) ≤ 4 * b * F.leaves

A cleaner consequence: (n - b) (n - 2 b - 1) ≤ 4 b · leaves.

The asymptotic statement

theorem Algebraic.Nechiporuk.natLog_le_logb (m : ℕ) : ↑(Nat.log 2 m) ≤ Real.logb 2 ↑m

The natural binary logarithm is at most the real one.

theorem Algebraic.Nechiporuk.eventually_sq_le_leaves (f : (n : ℕ) → Cslib.BooleanFunction n) (K : ℕ → ℕ) (c : ℕ) (hK : ∀ᶠ (n : ℕ) in Filter.atTop, K n ≤ n ^ c) (hacc : ∀ᶠ (n : ℕ) in Filter.atTop, 2 ^ (n - 2) ≤ (Cutwidth.accepting (f n)).card) (hrect : ∀ᶠ (n : ℕ) in Filter.atTop, Cutwidth.RectangleFree (f n) (K n)) : ∀ᶠ (n : ℕ) in Filter.atTop, ∀ (F : Binary.Formula n), F.Computes (f n) → ↑n ^ 2 ≤ 64 * (↑c + 3) * Real.logb 2 ↑n * ↑F.leaves

Formula size Ω(n² / log n) for rectangle-free families. For a family that is K n-rectangle-free with K n ≤ n ^ c and at least 2 ^ (n - 2) accepting inputs, every formula over the full binary basis computing f n has at least n² / (64 (c + 3) log₂ n) leaves, for all large n.