Strong Sensitivity Conjecture (bs(f) ≤ s(f)^2)

This file formalizes the strong sensitivity conjecture, asserting:

For every Boolean function f : {0,1}^n → {0,1}, bs(f) ≤ s(f)^2, where bs(f) denotes block sensitivity and s(f) denotes sensitivity.

Huang's theorem proves a quartic upper bound, bs(f) ≤ s(f)^4, thereby resolving the most widely known form of the sensitivity conjecture.

We now ask whether a stronger upper bound holds. Interestingly, the original paper of Nisan and Szegedy, where the sensitivity conjecture first appeared, already speculated that a quadratic upper bound might be the correct relation. On the lower bound side, Rubinstein (https://link.springer.com/article/10.1007/BF01200762) constructed Boolean functions exhibiting the first quadratic separation. The best currently known gap, due to Ambainis and Sun (https://arxiv.org/abs/1108.3494), is bs(f) ≥ (2/3)⋅s(f)^2.

References:

• Induced Subgraphs of Hypercubes and a Proof of the Sensitivity Conjecture by Hao Huang (see Section 3, Concluding Remarks)
• Variations on the Sensitivity Conjecture by Pooya Hatami, Raghav Kulkarni, and Denis Pankratov (see Question 3.1)
• On the Degree of Boolean Functions as Real Polynomials by Noam Nisan, and Mario Szegedy (see Section 4, Open Problems)

def StrongSensitivityConjecture.flip {n : ℕ} (x : Fin n → Bool) (B : Finset (Fin n)) : Fin n → Bool

Flip operator, flip x B returns input x with bits in block B inverted.

Equations

• StrongSensitivityConjecture.flip x B i = if i ∈ B then !x i else x i

def StrongSensitivityConjecture.sensitivityAt {n : ℕ} (f : (Fin n → Bool) → Bool) (x : Fin n → Bool) : ℕ

Local sensitivity s(f,x), number of indices where flipping one bit changes the value of f.

Equations

• StrongSensitivityConjecture.sensitivityAt f x = {i : Fin n | f (StrongSensitivityConjecture.flip x {i}) ≠ f x}.card

def StrongSensitivityConjecture.sensitivity {n : ℕ} (f : (Fin n → Bool) → Bool) : ℕ

Global sensitivity s(f), maximum sensitivity of f over all inputs.

Equations

• StrongSensitivityConjecture.sensitivity f = Finset.univ.sup (StrongSensitivityConjecture.sensitivityAt f)

def StrongSensitivityConjecture.IsValidBlockConfig {n : ℕ} (f : (Fin n → Bool) → Bool) (x : Fin n → Bool) (cB : Finset (Finset (Fin n))) : Prop

Check validity of block collection (disjoint and sensitive), A collection of blocks cB is valid for f at x if the blocks are disjoint and flipping any block changes f(x).

Equations

• StrongSensitivityConjecture.IsValidBlockConfig f x cB = ((↑cB).PairwiseDisjoint id ∧ ∀ B ∈ cB, f (StrongSensitivityConjecture.flip x B) ≠ f x)

noncomputable def StrongSensitivityConjecture.blockSensitivityAt {n : ℕ} (f : (Fin n → Bool) → Bool) (x : Fin n → Bool) : ℕ

Local block sensitivity bs(f,x), maximum size of a collection of sensitive, disjoint blocks for f at x.

Equations

• StrongSensitivityConjecture.blockSensitivityAt f x = {cB : Finset (Finset (Fin n)) | StrongSensitivityConjecture.IsValidBlockConfig f x cB}.sup Finset.card

noncomputable def StrongSensitivityConjecture.blockSensitivity {n : ℕ} (f : (Fin n → Bool) → Bool) : ℕ

Global block sensitivity of f, maximum block sensitivity of f over all inputs.

Equations

• StrongSensitivityConjecture.blockSensitivity f = Finset.univ.sup (StrongSensitivityConjecture.blockSensitivityAt f)

theorem StrongSensitivityConjecture.strong_sensitivity_conjecture {n : ℕ} (f : (Fin n → Bool) → Bool) : blockSensitivity f ≤ sensitivity f ^ 2

Strong Sensitivity Conjecture, for every Boolean function f : {0,1}^n → {0,1}, bs(f) ≤ s(f)^2.

We call this the strong sensitivity conjecture because the original sensitivity conjecture only asked for a polynomial bound in terms of s(f). Huang's celebrated result (often called the sensitivity theorem) gives a quartic bound, bs(f) ≤ s(f)^4, thereby settling the original conjecture.

def StrongSensitivityConjecture.nisanExample (n : ℕ) (x : Fin n → Bool) : Bool

Simple test example, A Boolean function whose block sensitivity is strictly greater than its sensitivity. Source: Nisan1989.

nisanExample(x) = 1 iff the Hamming weight of x is either n/2 or n/2 + 1. We assume n is a multiple of 4. The function is symmetric, so its value only depends on the Hamming weight of the input.

Equations

• StrongSensitivityConjecture.nisanExample n x = decide ({i : Fin n | x i = true}.card ∈ {n / 2, n / 2 + 1})

theorem StrongSensitivityConjecture.nisanExample_sensitivity (n : ℕ) (hn : 4 ∣ n) : sensitivity (nisanExample n) = n / 2

Assuming n is a multiple of 4, the sensitivity of nisanExample is n/2, achieved by any x with Hamming weight n/2.

theorem StrongSensitivityConjecture.nisanExample_blockSensitivity (n : ℕ) (hn : 4 ∣ n) : blockSensitivity (nisanExample n) = 3 * n / 4

Assuming n is a multiple of 4, the block sensitivity of nisanExample is 3n/4, achieved by any x with Hamming weight n/2. An optimal block configuration uses all n/2 1-bits as singleton blocks and forms n/4 disjoint size-2 blocks from the 0-bits.