Andreev's formula lower bound

Andreev's function Boolean.andreev b m on 2 ^ b + b * m bits treats its first 2 ^ b bits as the truth table of a b-bit Boolean function h, divides its remaining b * m bits into b blocks of m bits, computes the parity of each block, and evaluates h on the resulting b-bit string [And87], Jukna, Section 6.5, Arora and Barak, Section 14.3.

Fixing the first 2 ^ b bits to the truth table of any function h : BooleanFunction b leaves the b * m block variables free. If a further restriction ρ leaves at least one free variable in each of the b blocks, substituting a literal ± x_j for one surviving variable in block j and 0 for all other free variables turns any formula for (andreev b m)↾ρ into a formula for h without increasing its leaf size (Boolean.formulaSize_le_of_andreevBlock_nonempty).

Choosing a uniformly random extension leaving k = b * r variables free (with 2 * b ≤ 2 ^ r, for instance r = ⌊log₂ b⌋ + 2), the fraction of extensions that fix an entire m-bit block is at most C(b m - m, b r) / C(b m, b r) ≤ (1 - 1 / b) ^ (b r) ≤ 2 ^ (-r) ≤ 1 / (2 b). By a union bound, at least half of all extensions leave every block nonempty, so Subbotovskaya's average shrinkage (Boolean.exists_mem_formulaSize_sub_sq_le) yields a single restriction that both preserves a free variable in every block and shrinks the formula size by (r / m) ^ (3 / 2): (L(h) - 2 b r) ^ 2 * m ^ 3 ≤ 4 * L(andreev b m) ^ 2 * r ^ 3 (Boolean.formulaSize_sub_sq_mul_pow_three_le_andreev).

Combining this universal reduction with Shannon's counting theorem on b bits (Boolean.exists_hard_function_formulaSize) gives Andreev's n ^ (5 / 2 - o(1)) lower bound for an explicit function (Boolean.pow_two_mul_pow_three_le_formulaSize_andreev_sq, Boolean.two_pow_five_mul_le_formulaSize_andreev_sq).

Main definitions

• Cslib.Circuits.Boolean.andreevTableIndex: the 2 ^ b truth-table input coordinates of Andreev's function.
• Cslib.Circuits.Boolean.andreevBlockVar, Cslib.Circuits.Boolean.andreevBlock: the b blocks of m parity variables in Andreev's function.
• Cslib.Circuits.Boolean.andreev: Andreev's function on 2 ^ b + b * m bits.
• Cslib.Circuits.Boolean.andreevFixTable: the partial assignment fixing the 2 ^ b truth-table coordinates of andreev b m to the truth table of h : BooleanFunction b.

Main results

• Cslib.Circuits.Boolean.formulaSize_le_of_andreevBlock_nonempty: if ρ extends andreevFixTable b m h and leaves at least one variable of each block free, then L(h) ≤ L((andreev b m)↾ρ).
• Cslib.Circuits.Boolean.formulaSize_sub_sq_mul_pow_three_le_andreev: for every h : BooleanFunction b, 1 ≤ b, 1 ≤ r ≤ m, and 2 * b ≤ 2 ^ r, (L(h) - 2 b r) ^ 2 * m ^ 3 ≤ 4 * L(andreev b m) ^ 2 * r ^ 3.
• Cslib.Circuits.Boolean.exists_hard_function_formulaSize: for all sufficiently large b, some h : BooleanFunction b satisfies 2 ^ b < 3 * b * L(h).
• Cslib.Circuits.Boolean.pow_two_mul_pow_three_le_formulaSize_andreev_sq, Cslib.Circuits.Boolean.two_pow_five_mul_le_formulaSize_andreev_sq: Andreev's explicit n ^ (5 / 2 - o(1)) De Morgan formula size lower bound.

References

• A. E. Andreev, On a Method for Obtaining More Than Quadratic Effective Lower Bounds for the Complexity of π-Schemes
• S. Jukna, Boolean Function Complexity: Advances and Frontiers
• S. Arora and B. Barak, Computational Complexity: A Modern Approach

Andreev's function and truth-table restrictions

def Cslib.Circuits.Boolean.andreevTableIndex (b m : ℕ) (idx : Fin (2 ^ b)) : Fin (2 ^ b + b * m)

The idx-th truth-table coordinate among the 2 ^ b + b * m inputs of Andreev's function.

def Cslib.Circuits.Boolean.andreevBlockVar (b m : ℕ) (j : Fin b) (t : Fin m) : Fin (2 ^ b + b * m)

The t-th variable of the j-th parity block among the 2 ^ b + b * m inputs of Andreev's function.

def Cslib.Circuits.Boolean.andreevBlock (b m : ℕ) (j : Fin b) : Finset (Fin (2 ^ b + b * m))

The m input coordinates forming the j-th parity block of Andreev's function.

def Cslib.Circuits.Boolean.andreev (b m : ℕ) : BooleanFunction (2 ^ b + b * m)

Andreev's function on 2 ^ b + b * m bits: the first 2 ^ b bits encode the truth table of a b-bit function (indexed via BitString.equivFin b), and the remaining b * m bits form b blocks of m bits whose parities are fed as the b-bit input to that truth table.

theorem Cslib.Circuits.Boolean.andreevBlockVar_injective (b m : ℕ) (j : Fin b) : Function.Injective (andreevBlockVar b m j)

@[simp]

theorem Cslib.Circuits.Boolean.card_andreevBlock (b m : ℕ) (j : Fin b) : (andreevBlock b m j).card = m

def Cslib.Circuits.Boolean.andreevFixTable (b m : ℕ) (h : BooleanFunction b) : BitString.PartialAssignment (Fin (2 ^ b + b * m))

The partial assignment fixing the first 2 ^ b inputs of andreev b m to the truth table of h : BooleanFunction b and leaving all b * m block inputs free.

@[simp]

theorem Cslib.Circuits.Boolean.andreevFixTable_tableIndex (b m : ℕ) (h : BooleanFunction b) (idx : Fin (2 ^ b)) : andreevFixTable b m h (andreevTableIndex b m idx) = some (h ((BitString.equivFin b).symm idx))

@[simp]

theorem Cslib.Circuits.Boolean.andreevFixTable_natAdd (b m : ℕ) (h : BooleanFunction b) (u : Fin (b * m)) : andreevFixTable b m h (Fin.natAdd (2 ^ b) u) = none

@[simp]

theorem Cslib.Circuits.Boolean.andreevFixTable_blockVar (b m : ℕ) (h : BooleanFunction b) (j : Fin b) (t : Fin m) : andreevFixTable b m h (andreevBlockVar b m j t) = none

theorem Cslib.Circuits.Boolean.free_andreevFixTable (b m : ℕ) (h : BooleanFunction b) : (andreevFixTable b m h).free = Finset.image (Fin.natAdd (2 ^ b)) Finset.univ

@[simp]

theorem Cslib.Circuits.Boolean.card_free_andreevFixTable (b m : ℕ) (h : BooleanFunction b) : (andreevFixTable b m h).free.card = b * m

theorem Cslib.Circuits.Boolean.andreevBlock_subset_free_andreevFixTable (b m : ℕ) (h : BooleanFunction b) (j : Fin b) : andreevBlock b m j ⊆ (andreevFixTable b m h).free

theorem Cslib.Circuits.Boolean.andreev_fill_of_extends {b m : ℕ} {h : BooleanFunction b} {ρ : BitString.PartialAssignment (Fin (2 ^ b + b * m))} (hext : ρ.Extends (andreevFixTable b m h)) (w : BitString (2 ^ b + b * m)) : andreev b m (ρ.fill w) = h fun (j : Fin b) => parity m fun (t : Fin m) => ρ.fill w (andreevBlockVar b m j t)

Under any extension ρ of andreevFixTable b m h, Andreev's function evaluates h on the block parities of ρ.fill w.

Projection from non-eliminated parity blocks

theorem Cslib.Circuits.Boolean.formulaSize_le_of_andreevBlock_nonempty {b m : ℕ} {h : BooleanFunction b} {ρ : BitString.PartialAssignment (Fin (2 ^ b + b * m))} (hext : ρ.Extends (andreevFixTable b m h)) (hblocks : ∀ (j : Fin b), (ρ.free ∩ andreevBlock b m j).Nonempty) : formulaSize h ≤ formulaSize (andreev b m ∘ ρ.fill)

Andreev's projection lemma: if ρ extends andreevFixTable b m h and leaves at least one variable in each of the b parity blocks free, then h is obtained from (andreev b m)↾ρ by substituting a single literal for one free variable in each block and false for all other inputs. Consequently, L(h) ≤ L((andreev b m)↾ρ).

Andreev's reduction and explicit formula lower bound

theorem Cslib.Circuits.Boolean.formulaSize_sub_sq_mul_pow_three_le_andreev {b : ℕ} (h : BooleanFunction b) (hb : 1 ≤ b) {m r : ℕ} (hr1 : 1 ≤ r) (hrm : r ≤ m) (hbr : 2 * b ≤ 2 ^ r) : (formulaSize h - 2 * b * r) ^ 2 * m ^ 3 ≤ 4 * formulaSize (andreev b m) ^ 2 * r ^ 3

Andreev's reduction theorem: for every b-bit Boolean function h, 1 ≤ b, 1 ≤ r ≤ m, and 2 * b ≤ 2 ^ r, the formula size of andreev b m satisfies (L(h) - 2 * b * r) ^ 2 * m ^ 3 ≤ 4 * L(andreev b m) ^ 2 * r ^ 3 [And87], Jukna, Theorem 6.14.

theorem Cslib.Circuits.Boolean.formulaSize_sub_sq_mul_pow_three_le_andreev_log {b : ℕ} (h : BooleanFunction b) (hb : 1 ≤ b) {m : ℕ} (hm : Nat.log 2 b + 2 ≤ m) : (formulaSize h - 2 * b * (Nat.log 2 b + 2)) ^ 2 * m ^ 3 ≤ 4 * formulaSize (andreev b m) ^ 2 * (Nat.log 2 b + 2) ^ 3

Specialization of Andreev's reduction to r = Nat.log 2 b + 2, for which 2 * b ≤ 2 ^ r always holds.

theorem Cslib.Circuits.Boolean.exists_hard_function_formulaSize : ∃ (B : ℕ), ∀ b ≥ B, ∃ (h : BooleanFunction b), 2 ^ b < 3 * b * formulaSize h

Shannon's counting bound for formula leaf size: for all sufficiently large b, some Boolean function h on b bits satisfies 2 ^ b < 3 * b * L(h).

theorem Cslib.Circuits.Boolean.pow_two_mul_pow_three_le_formulaSize_andreev_sq : ∃ (B : ℕ), ∀ b ≥ B, ∀ m ≥ Nat.log 2 b + 2, 2 ^ (2 * b) * m ^ 3 ≤ 144 * b ^ 2 * (Nat.log 2 b + 2) ^ 3 * formulaSize (andreev b m) ^ 2

Andreev's explicit formula lower bound: for all sufficiently large b and all block sizes m ≥ ⌊log₂ b⌋ + 2, the formula size of andreev b m satisfies 2 ^ (2 * b) * m ^ 3 ≤ 144 * b ^ 2 * (⌊log₂ b⌋ + 2) ^ 3 * L(andreev b m) ^ 2 [And87], Jukna, Theorem 6.14.

theorem Cslib.Circuits.Boolean.two_pow_five_mul_le_formulaSize_andreev_sq : ∃ (B : ℕ), ∀ b ≥ B, 2 ^ (5 * b) ≤ 144 * b ^ 2 * (Nat.log 2 b + 2) ^ 3 * formulaSize (andreev b (2 ^ b)) ^ 2

Andreev's n ^ (5 / 2 - o(1)) lower bound at block size m = 2 ^ b (input length n = (b + 1) * 2 ^ b): for all sufficiently large b, 2 ^ (5 * b) ≤ 144 * b ^ 2 * (⌊log₂ b⌋ + 2) ^ 3 * L(andreev b (2 ^ b)) ^ 2.