Superquadratic sensitivity separation: separation

The final separation statements. For each depth d ≥ 1 there is a nonconstant Boolean function whose block sensitivity at the all-false input is at least 2 ^ d / (4 * (d + 2) ^ 2) times the square of its sensitivity. Consequently block sensitivity is not bounded by C * sensitivity ^ 2 for any constant C, and there is even a fixed exponent α > 2 with s(f) ^ α ≤ bs(f, 0) along a family of functions of unbounded block sensitivity. Here s(f) is sensitivity f and bs(f, 0) is the block sensitivity at the all-false input.

Main results

• quantitative_separation: for d ≥ 1, some nonconstant function has bs(f, 0) / s(f) ^ 2 ≥ 2 ^ d / (4 * (d + 2) ^ 2).
• unbounded_quadratic_separation: for every C, some nonconstant function has C * s(f) ^ 2 < bs(f, 0).
• fixed_power_separation: for a fixed α > 2, a family of nonconstant functions with s(F m) ^ α ≤ bs(F m, 0) and unbounded block sensitivity at the all-false input.

References

• Adapted from OpenAI's formalization [OAI26b] at revision adc7f1241b42e322a6451854ab7e4b4c146bf78a (file lean/OAI/Combinatorics/Sensitivity/Separation.lean), via the complexitylib port [Sch26e] at revision add0aca8ee0d71e68969f2cb45cf91554a50f787.

theorem Cslib.QueryComplexity.SensitivitySeparation.Internal.quantitative_separation (d : ℕ) (hd : 1 ≤ d) : ∃ (n : ℕ) (f : (Fin n → Bool) → Bool), 0 < n ∧ (f fun (x : Fin n) => false) = false ∧ (∃ (x : Fin n → Bool) (y : Fin n → Bool), f x ≠ f y) ∧ 2 ^ d / (4 * (↑d + 2) ^ 2) ≤ ↑(blockSensitivityAt f fun (x : Fin n) => false) / ↑(sensitivity f) ^ 2

For 1 ≤ d there is a nonconstant f : (Fin n → Bool) → Bool with 0 < n, f (fun _ => false) = false and 2 ^ d / (4 * (d + 2) ^ 2) ≤ blockSensitivityAt f (fun _ => false) / sensitivity f ^ 2.

theorem Cslib.QueryComplexity.SensitivitySeparation.Internal.unbounded_quadratic_separation (C : ℝ) : ∃ (n : ℕ) (f : (Fin n → Bool) → Bool), 0 < n ∧ (f fun (x : Fin n) => false) = false ∧ (∃ (x : Fin n → Bool) (y : Fin n → Bool), f x ≠ f y) ∧ C * ↑(sensitivity f) ^ 2 < ↑(blockSensitivityAt f fun (x : Fin n) => false)

For every C there is a nonconstant f : (Fin n → Bool) → Bool with 0 < n, f (fun _ => false) = false and C * sensitivity f ^ 2 < blockSensitivityAt f (fun _ => false).

theorem Cslib.QueryComplexity.SensitivitySeparation.Internal.fixed_power_separation : ∃ (α : ℝ), 2 < α ∧ ∃ (n : ℕ → ℕ) (F : (m : ℕ) → (Fin (n m) → Bool) → Bool), (∀ (m : ℕ), 0 < n m ∧ (F m fun (x : Fin (n m)) => false) = false ∧ (∃ (x : Fin (n m) → Bool) (y : Fin (n m) → Bool), F m x ≠ F m y) ∧ ↑(sensitivity (F m)) ^ α ≤ ↑(blockSensitivityAt (F m) fun (x : Fin (n m)) => false)) ∧ Filter.Tendsto (fun (m : ℕ) => ↑(blockSensitivityAt (F m) fun (x : Fin (n m)) => false)) Filter.atTop Filter.atTop

There are α > 2 and Boolean functions F m on n m variables such that for every m, 0 < n m, F m is nonconstant, vanishes at the all-false input and satisfies sensitivity (F m) ^ α ≤ blockSensitivityAt (F m) (fun _ => false), while blockSensitivityAt (F m) (fun _ => false) tends to infinity.