Subbotovskaya's random restriction method

Fixing a variable i of a reduced De Morgan formula to a random constant removes the ℓ_i leaves labelled by i, and for each such leaf that feeds a binary gate, the constant annihilates the gate under one of the two values of i, eliminating the gate's other argument as well. Subbotovskaya [Sub61] used this observation to show that a formula of least leaf size L ≥ 2 shrinks on average by at least 3 L / (2 s) leaves when one of its s variables is fixed at random (Formula.IsLeafMinimal.leafSize_restrictAt_false_add_true_le, Boolean.sum_formulaSize_restrict_update_le), and therefore that restricting to k variables shrinks the formula size by a factor of (k / n) ^ (3 / 2) Jukna, Lemma 6.12.

Stated without fractional powers by squaring both sides, every Boolean function on n bits and every 1 ≤ k ≤ n has a partial assignment with k free bits under which L(f↾ρ) ^ 2 * n ^ 3 ≤ L(f) ^ 2 * k ^ 3 (Boolean.exists_withFree_formulaSize_sq_mul_pow_three_le). Taking k = 1 gives Subbotovskaya's n ^ (3 / 2) lower bound for parity (Boolean.pow_three_le_formulaSize_parity_sq), the first superlinear formula lower bound. Averaging over all extensions with k free bits bounds the average restricted formula size, ready to be combined with a union bound in Andreev's theorem (Boolean.sum_extensions_formulaSize_sub_sq_le, Boolean.exists_mem_formulaSize_sub_sq_le).

Main definitions

• Cslib.Circuits.Formula.restrictAt: restrict a De Morgan formula by fixing one input to a Boolean constant.
• Cslib.Circuits.Formula.IsLeafMinimal: formulas whose leaf size is the least among all formulas computing the same function.

Main results

• Cslib.Circuits.Formula.IsLeafMinimal.leafSize_restrictAt_false_add_true_le: fixing input i to false and true in a leaf-minimal formula that is not a single i-leaf gives L(F↾(i = 0)) + L(F↾(i = 1)) + 3 ℓ_i(F) ≤ 2 L(F).
• Cslib.Circuits.Boolean.sum_formulaSize_restrict_update_le: summing over s free inputs bounds restricted formula sizes by (2 s - 3) L(f↾ρ) when L(f↾ρ) ≠ 1 (and 2 s - 2 when L = 1).
• Cslib.Circuits.Boolean.exists_extensions_formulaSize_sq_mul_pow_three_le, Cslib.Circuits.Boolean.exists_withFree_formulaSize_sq_mul_pow_three_le: Subbotovskaya's shrinkage lemma for k surviving free inputs.
• Cslib.Circuits.Boolean.pow_three_le_formulaSize_parity_sq, Cslib.Circuits.Boolean.pow_three_le_leafSize_sq_of_computes_parity: Subbotovskaya's n ^ (3 / 2) formula leaf-size lower bound for parity.
• Cslib.Circuits.Boolean.sum_extensions_formulaSize_sub_sq_le, Cslib.Circuits.Boolean.exists_mem_formulaSize_sub_sq_le: average shrinkage over all extensions leaving k inputs free, and existence of a small restriction inside any dense subset.

References

• B. A. Subbotovskaya, Realizations of Linear Functions by Formulas Using ∨, &, -
• S. Jukna, Boolean Function Complexity: Advances and Frontiers

Restricting a single input

def Cslib.Circuits.Formula.restrictAt {n : ℕ} (i : Fin n) (b : Bool) (F : Formula Boolean.signature n) : Formula Boolean.signature n

Restrict a De Morgan formula by fixing input i to b and leaving all other inputs free.

@[simp]

theorem Cslib.Circuits.Formula.eval_restrictAt {n : ℕ} (i : Fin n) (b : Bool) (F : Formula Boolean.signature n) (x : BitString n) : (restrictAt i b F).eval Boolean.interpretation x = F.eval Boolean.interpretation (Function.update x i b)

theorem Cslib.Circuits.Formula.leafSize_restrictAt_add_leafSizeIn_le {n : ℕ} (F : Formula Boolean.signature n) (i : Fin n) (b : Bool) : (restrictAt i b F).leafSize + leafSizeIn {i} F ≤ F.leafSize

@[simp]

theorem Cslib.Circuits.Formula.restrictAt_const {n : ℕ} (i : Fin n) (b c : Bool) : restrictAt i b (const c) = const c

@[simp]

theorem Cslib.Circuits.Formula.restrictAt_not {n : ℕ} (i : Fin n) (b : Bool) (F : Formula Boolean.signature n) : restrictAt i b F.not = (restrictAt i b F).mkNot

@[simp]

theorem Cslib.Circuits.Formula.restrictAt_and {n : ℕ} (i : Fin n) (b : Bool) (F G : Formula Boolean.signature n) : restrictAt i b (F.and G) = (restrictAt i b F).mkAnd (restrictAt i b G)

@[simp]

theorem Cslib.Circuits.Formula.restrictAt_or {n : ℕ} (i : Fin n) (b : Bool) (F G : Formula Boolean.signature n) : restrictAt i b (F.or G) = (restrictAt i b F).mkOr (restrictAt i b G)

theorem Cslib.Circuits.Formula.restrictAt_input_self {n : ℕ} (i : Fin n) (b : Bool) : restrictAt i b (input i) = const b

theorem Cslib.Circuits.Formula.restrictAt_input_of_ne {n : ℕ} {i j : Fin n} (h : j ≠ i) (b : Bool) : restrictAt i b (input j) = input j

Leaf-minimal formulas

def Cslib.Circuits.Formula.IsLeafMinimal {n : ℕ} (F : Formula Boolean.signature n) : Prop

A De Morgan formula is leaf-minimal when no formula with fewer leaves computes the same Boolean function.

theorem Cslib.Circuits.Formula.isLeafMinimal_iff_leafSize_eq_formulaSize {n : ℕ} {F : Formula Boolean.signature n} : F.IsLeafMinimal ↔ F.leafSize = Boolean.formulaSize (F.eval Boolean.interpretation)

A formula is leaf-minimal exactly when its leaf size equals the formula size of the function it computes.

theorem Cslib.Circuits.Formula.IsLeafMinimal.arg {n : ℕ} {op : Boolean.Op} {args : Fin (Boolean.signature.Arity op) → Formula Boolean.signature n} (hF : (gate op args).IsLeafMinimal) (j : Fin (Boolean.signature.Arity op)) : (args j).IsLeafMinimal

Every argument of a leaf-minimal gate is leaf-minimal.

theorem Cslib.Circuits.Formula.IsLeafMinimal.of_not {n : ℕ} {F : Formula Boolean.signature n} (h : F.not.IsLeafMinimal) : F.IsLeafMinimal

theorem Cslib.Circuits.Formula.IsLeafMinimal.left_of_and {n : ℕ} {F G : Formula Boolean.signature n} (h : (F.and G).IsLeafMinimal) : F.IsLeafMinimal

theorem Cslib.Circuits.Formula.IsLeafMinimal.right_of_and {n : ℕ} {F G : Formula Boolean.signature n} (h : (F.and G).IsLeafMinimal) : G.IsLeafMinimal

theorem Cslib.Circuits.Formula.IsLeafMinimal.left_of_or {n : ℕ} {F G : Formula Boolean.signature n} (h : (F.or G).IsLeafMinimal) : F.IsLeafMinimal

theorem Cslib.Circuits.Formula.IsLeafMinimal.right_of_or {n : ℕ} {F G : Formula Boolean.signature n} (h : (F.or G).IsLeafMinimal) : G.IsLeafMinimal

Single-step shrinkage

theorem Cslib.Circuits.Formula.IsLeafMinimal.leafSize_restrictAt_false_add_true_le {n : ℕ} {F : Formula Boolean.signature n} (hF : F.IsLeafMinimal) (i : Fin n) (hnu : ¬(F.leafSize = 1 ∧ leafSizeIn {i} F = 1)) : (restrictAt i false F).leafSize + (restrictAt i true F).leafSize + 3 * leafSizeIn {i} F ≤ 2 * F.leafSize

Subbotovskaya's single-variable shrinkage on a leaf-minimal formula: for every input i, unless F has a single leaf and that leaf is at i, the restrictions of F fixing i to false and true satisfy L(F↾(i = 0)) + L(F↾(i = 1)) + 3 ℓ_i(F) ≤ 2 L(F).

theorem Cslib.Circuits.Boolean.sum_formulaSize_restrict_update_le {n : ℕ} (f : BooleanFunction n) (ρ : BitString.PartialAssignment (Fin n)) : (∑ i ∈ ρ.free, (formulaSize (f ∘ BitString.PartialAssignment.fill (Function.update ρ i (some false))) + formulaSize (f ∘ BitString.PartialAssignment.fill (Function.update ρ i (some true)))) + if formulaSize (f ∘ ρ.fill) = 1 then 2 else 3 * formulaSize (f ∘ ρ.fill)) ≤ 2 * ρ.free.card * formulaSize (f ∘ ρ.fill)

Summed over the free inputs of ρ, the formula sizes after fixing one free input of ρ satisfy Subbotovskaya's single-step shrinkage inequality:

• when L(f↾ρ) ≠ 1, the sum plus 3 L(f↾ρ) is at most 2 |ρ.free| L(f↾ρ);
• when L(f↾ρ) = 1, some free input has the single leaf and fixing it reduces the formula size to 0, while the other |ρ.free| - 1 free inputs contribute at most 2 each.

theorem Cslib.Circuits.Boolean.sum_formulaSize_restrict_update_le_add_one {n : ℕ} (f : BooleanFunction n) (ρ : BitString.PartialAssignment (Fin n)) : ∑ i ∈ ρ.free, (formulaSize (f ∘ BitString.PartialAssignment.fill (Function.update ρ i (some false))) + formulaSize (f ∘ BitString.PartialAssignment.fill (Function.update ρ i (some true)))) ≤ (2 * ρ.free.card - 3) * formulaSize (f ∘ ρ.fill) + 1

Uniform single-step shrinkage inequality valid for every formula size, including 1: the sum over all 2 |ρ.free| single-variable extensions of ρ is at most (2 |ρ.free| - 3) L(f↾ρ) + 1.

Deterministic shrinkage and Subbotovskaya's parity lower bound

theorem Cslib.Circuits.Boolean.exists_mem_free_formulaSize_sq_mul_pow_three_le {n : ℕ} (f : BooleanFunction n) {ρ : BitString.PartialAssignment (Fin n)} (hs : 2 ≤ ρ.free.card) : ∃ i ∈ ρ.free, ∃ (b : Bool), formulaSize (f ∘ BitString.PartialAssignment.fill (Function.update ρ i (some b))) ^ 2 * ρ.free.card ^ 3 ≤ formulaSize (f ∘ ρ.fill) ^ 2 * (ρ.free.card - 1) ^ 3

When |ρ.free| ≥ 2, fixing some free coordinate of ρ to a constant shrinks the formula size so that L' ^ 2 * s ^ 3 ≤ L ^ 2 * (s - 1) ^ 3 for s = |ρ.free|.

theorem Cslib.Circuits.Boolean.exists_extensions_formulaSize_sq_mul_pow_three_le {n : ℕ} (f : BooleanFunction n) (ρ₀ : BitString.PartialAssignment (Fin n)) {k : ℕ} (hk1 : 1 ≤ k) (hk : k ≤ ρ₀.free.card) : ∃ ρ ∈ ρ₀.extensions k, formulaSize (f ∘ ρ.fill) ^ 2 * ρ₀.free.card ^ 3 ≤ formulaSize (f ∘ ρ₀.fill) ^ 2 * k ^ 3

Subbotovskaya's shrinkage lemma for extensions of a partial assignment ρ₀: for every 1 ≤ k ≤ |ρ₀.free|, some extension ρ of ρ₀ with k free inputs satisfies L(f↾ρ) ^ 2 * |ρ₀.free| ^ 3 ≤ L(f↾ρ₀) ^ 2 * k ^ 3.

theorem Cslib.Circuits.Boolean.exists_withFree_formulaSize_sq_mul_pow_three_le {n : ℕ} (f : BooleanFunction n) {k : ℕ} (hk1 : 1 ≤ k) (hk : k ≤ n) : ∃ ρ ∈ BitString.PartialAssignment.withFree (Fin n) k, formulaSize (f ∘ ρ.fill) ^ 2 * n ^ 3 ≤ formulaSize f ^ 2 * k ^ 3

Subbotovskaya's shrinkage lemma: for every Boolean function f on n bits and every 1 ≤ k ≤ n, some partial assignment ρ leaving k inputs free satisfies L(f↾ρ) ^ 2 * n ^ 3 ≤ L(f) ^ 2 * k ^ 3.

theorem Cslib.Circuits.Boolean.pow_three_le_formulaSize_parity_sq (n : ℕ) : n ^ 3 ≤ formulaSize (parity n) ^ 2

Subbotovskaya's parity lower bound: the formula size of parity n is at least n ^ (3 / 2), stated as n ^ 3 ≤ L(parity n) ^ 2 [Sub61], Jukna, Section 6.3.

theorem Cslib.Circuits.Boolean.pow_three_le_leafSize_sq_of_computes_parity {n : ℕ} {F : Formula signature n} (hF : F.Computes interpretation (parity n)) : n ^ 3 ≤ F.leafSize ^ 2

Subbotovskaya's parity lower bound for De Morgan formulas: every formula computing parity n has leaf size L satisfying n ^ 3 ≤ L ^ 2.

Average shrinkage over random restrictions

theorem Cslib.Circuits.Boolean.sum_extensions_formulaSize_sub_sq_le {n : ℕ} (f : BooleanFunction n) (ρ₀ : BitString.PartialAssignment (Fin n)) {k : ℕ} (hk1 : 1 ≤ k) (hk : k ≤ ρ₀.free.card) : (∑ ρ ∈ ρ₀.extensions k, formulaSize (f ∘ ρ.fill) - k * (ρ₀.extensions k).card) ^ 2 * ρ₀.free.card ^ 3 ≤ formulaSize (f ∘ ρ₀.fill) ^ 2 * k ^ 3 * (ρ₀.extensions k).card ^ 2

Subbotovskaya's average shrinkage over all extensions of ρ₀ with k free inputs: for 1 ≤ k ≤ |ρ₀.free|, the sum S_k = ∑ ρ ∈ ρ₀.extensions k, L(f↾ρ) and the count N_k = |ρ₀.extensions k| satisfy (S_k - k * N_k) ^ 2 * |ρ₀.free| ^ 3 ≤ L(f↾ρ₀) ^ 2 * k ^ 3 * N_k ^ 2.

theorem Cslib.Circuits.Boolean.exists_mem_formulaSize_sub_sq_le {n : ℕ} (f : BooleanFunction n) (ρ₀ : BitString.PartialAssignment (Fin n)) {k : ℕ} (hk1 : 1 ≤ k) (hk : k ≤ ρ₀.free.card) {A : Finset (BitString.PartialAssignment (Fin n))} (hAsub : A ⊆ ρ₀.extensions k) (hAcard : (ρ₀.extensions k).card ≤ 2 * A.card) : ∃ ρ ∈ A, (formulaSize (f ∘ ρ.fill) - 2 * k) ^ 2 * ρ₀.free.card ^ 3 ≤ 4 * formulaSize (f ∘ ρ₀.fill) ^ 2 * k ^ 3

If a subset A ⊆ ρ₀.extensions k has at least half the extensions (|ρ₀.extensions k| ≤ 2 |A|), then some ρ ∈ A has formula size bounded by Subbotovskaya's shrinkage: (L(f↾ρ) - 2 k) ^ 2 * |ρ₀.free| ^ 3 ≤ 4 * L(f↾ρ₀) ^ 2 * k ^ 3.