A superquadratic separation of block sensitivity from sensitivity

Every Boolean function satisfies s(f) ≤ bs(f) [Nis91], and Huang's theorem [Hua19] bounds block sensitivity polynomially in sensitivity (QueryComplexity.blockSensitivity_le_two_mul_sensitivity_pow_four). Rubinstein's function shows that bs(f) can be quadratic in s(f) [Rub95]. OpenAI's construction [OAI26b] goes beyond the square: for every constant C there is a nonconstant Boolean function f with bs(f) > C · s(f)², and there is a family whose block sensitivity is at least a fixed power α > 2 of its sensitivity.

Sensitivity here is CSLib's BitString.sensitivity, the maximum number of sensitive coordinates at a single input (not average sensitivity), and block sensitivity is CSLib's QueryComplexity.blockSensitivity. The blockSensitivityAt statements bound the block sensitivity at the all-false input, where the function takes the value false. The construction is carried out in the Internal modules with measures over arbitrary finite coordinate types; Internal.Bridge identifies those with CSLib's measures on Fin n.

Since bs(f) ≤ C(f) ≤ D(f), the same functions separate certificate complexity and deterministic decision-tree complexity from squared sensitivity. These consequences are short deductions from the separation.

Main results

• QueryComplexity.exists_two_pow_div_le_blockSensitivityAt_div_sensitivity_sq: for every d ≥ 1 there is a nonconstant f with bs(f, 0) / s(f) ^ 2 ≥ 2 ^ d / (4 (d + 2) ^ 2).
• QueryComplexity.exists_mul_sensitivity_sq_lt_blockSensitivityAt: for every C there is a nonconstant f with f 0 = false and C * s(f) ^ 2 < bs(f, 0).
• QueryComplexity.exists_mul_sensitivity_sq_lt_blockSensitivity: for every C there is a nonconstant f with C * s(f) ^ 2 < bs(f).
• QueryComplexity.exists_sensitivity_rpow_le_blockSensitivityAt: a family with s(f) ^ α ≤ bs(f) for a fixed α > 2 and unbounded block sensitivity.
• QueryComplexity.exists_mul_sensitivity_sq_lt_certificateComplexity: the same separation for certificate complexity.
• DecisionTree.exists_mul_sensitivity_sq_lt_complexity, DecisionTree.exists_sensitivity_rpow_le_complexity: the same separations for deterministic decision-tree complexity.

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.
• N. Nisan, CREW PRAMs and decision trees
• D. Rubinstein, Sensitivity vs. block sensitivity of Boolean functions
• H. Huang, Induced subgraphs of hypercubes and a proof of the Sensitivity Conjecture

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

Quantitative superquadratic separation: for every d ≥ 1 there is a nonconstant Boolean function f with f 0 = false and bs(f, 0) / s(f) ^ 2 ≥ 2 ^ d / (4 (d + 2) ^ 2).

theorem Cslib.QueryComplexity.exists_mul_sensitivity_sq_lt_blockSensitivityAt (C : ℝ) : ∃ (n : ℕ) (f : BooleanFunction n), 0 < n ∧ (f fun (x : Fin n) => false) = false ∧ (∃ (x : BitString n) (y : BitString n), f x ≠ f y) ∧ C * ↑(BitString.sensitivity f) ^ 2 < ↑(blockSensitivityAt f fun (x : Fin n) => false)

For every C there is a nonconstant Boolean function f with f 0 = false and C * s(f) ^ 2 < bs(f, 0).

theorem Cslib.QueryComplexity.exists_mul_sensitivity_sq_lt_blockSensitivity (C : ℝ) : ∃ (n : ℕ) (f : BooleanFunction n), 0 < n ∧ (∃ (x : BitString n) (y : BitString n), f x ≠ f y) ∧ C * ↑(BitString.sensitivity f) ^ 2 < ↑(blockSensitivity f)

Block sensitivity is not quadratically bounded by sensitivity: for every C there is a nonconstant Boolean function f with C * s(f) ^ 2 < bs(f).

theorem Cslib.QueryComplexity.exists_sensitivity_rpow_le_blockSensitivityAt : ∃ (α : ℝ), 2 < α ∧ ∃ (n : ℕ → ℕ) (F : (m : ℕ) → BooleanFunction (n m)), (∀ (m : ℕ), 0 < n m ∧ (F m fun (x : Fin (n m)) => false) = false ∧ (∃ (x : BitString (n m)) (y : BitString (n m)), F m x ≠ F m y) ∧ ↑(BitString.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

Fixed-power separation: for some α > 2 there is a family of nonconstant Boolean functions F m with F m 0 = false and s(F m) ^ α ≤ bs(F m, 0), whose block sensitivity at the all-false input tends to infinity.

theorem Cslib.QueryComplexity.exists_mul_sensitivity_sq_lt_certificateComplexity (C : ℝ) : ∃ (n : ℕ) (f : BooleanFunction n), 0 < n ∧ (∃ (x : BitString n) (y : BitString n), f x ≠ f y) ∧ C * ↑(BitString.sensitivity f) ^ 2 < ↑(certificateComplexity f)

Certificate complexity is not quadratically bounded by sensitivity: for every C there is a nonconstant Boolean function f with C * s(f) ^ 2 < C(f).

theorem Cslib.DecisionTree.exists_mul_sensitivity_sq_lt_complexity (C : ℝ) : ∃ (n : ℕ) (f : BooleanFunction n), 0 < n ∧ (∃ (x : BitString n) (y : BitString n), f x ≠ f y) ∧ C * ↑(BitString.sensitivity f) ^ 2 < ↑(complexity f)

Deterministic decision-tree complexity is not quadratically bounded by sensitivity: for every C there is a nonconstant Boolean function f with C * s(f) ^ 2 < D(f).

theorem Cslib.DecisionTree.exists_sensitivity_rpow_le_complexity : ∃ (α : ℝ), 2 < α ∧ ∃ (n : ℕ → ℕ) (F : (m : ℕ) → BooleanFunction (n m)), (∀ (m : ℕ), 0 < n m ∧ (∃ (x : BitString (n m)) (y : BitString (n m)), F m x ≠ F m y) ∧ ↑(BitString.sensitivity (F m)) ^ α ≤ ↑(complexity (F m))) ∧ Filter.Tendsto (fun (m : ℕ) => ↑(complexity (F m))) Filter.atTop Filter.atTop

Fixed-power separation of decision-tree complexity from sensitivity: for some α > 2 there is a family of nonconstant Boolean functions F m with s(F m) ^ α ≤ D(F m) and D(F m) → ∞.