/-
Copyright 2025 The Formal Conjectures Authors.
Licensed under the Apache License, Version 2.0 (the "License");
you may not use this file except in compliance with the License.
You may obtain a copy of the License at
https://www.apache.org/licenses/LICENSE-2.0
Unless required by applicable law or agreed to in writing, software
distributed under the License is distributed on an "AS IS" BASIS,
WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
See the License for the specific language governing permissions and
limitations under the License.
-/
import FormalConjecturesUtil
Strong Sensitivity Conjecture (bs(f) ≤ s(f)^2)
This file formalizes the
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 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 bs(f) ≥ (2/3)⋅s(f)^2.
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)
namespace StrongSensitivityConjecture
open Finset Function Classical
section Sensitivity
variable {n : ℕ}
Flip operator,
flip x B returns input x with bits in block B inverted.
def flip (x : Fin n → Bool) (B : Finset (Fin n)) : Fin n → Bool :=
fun i => if i ∈ B then !(x i) else x i
Local sensitivity s(f,x),
number of indices where flipping one bit changes the value of f.
def sensitivityAt (f : (Fin n → Bool) → Bool) (x : Fin n → Bool) : ℕ :=
#{i | f (flip x {i}) ≠ f x}
Global sensitivity s(f),
maximum sensitivity of f over all inputs.
def sensitivity (f : (Fin n → Bool) → Bool) : ℕ :=
univ.sup (sensitivityAt f)
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).
def IsValidBlockConfig (f : (Fin n → Bool) → Bool) (x : Fin n → Bool)
(cB : Finset (Finset (Fin n))) : Prop :=
(cB : Set (Finset (Fin n))).PairwiseDisjoint id ∧
∀ B ∈ cB, f (flip x B) ≠ f x
Local block sensitivity bs(f,x),
maximum size of a collection of sensitive, disjoint blocks for f at x.
noncomputable def blockSensitivityAt (f : (Fin n → Bool) → Bool) (x : Fin n → Bool) : ℕ :=
Finset.sup {cB | IsValidBlockConfig f x cB} card
Global block sensitivity of f,
maximum block sensitivity of f over all inputs.
noncomputable def blockSensitivity (f : (Fin n → Bool) → Bool) : ℕ :=
univ.sup (blockSensitivityAt f)
Strong Sensitivity Conjecture,
for every Boolean function f : {0,1}^n → {0,1},
bs(f) ≤ s(f)^2.
We call this the 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.
@[category research open, AMS 68]
theorem strong_sensitivity_conjecture {n : ℕ} (f : (Fin n → Bool) → Bool) :
blockSensitivity f ≤ sensitivity f ^ 2 := n:ℕf:(Fin n → Bool) → Bool⊢ blockSensitivity f ≤ sensitivity f ^ 2
All goals completed! 🐙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.
@[category test, AMS 68]
def nisanExample (n : ℕ) (x : Fin n → Bool) : Bool :=
let w := #{i | x i}
decide ((w : ℚ) ∈ ({(n / 2 : ℚ), (n / 2 : ℚ) + 1} : Finset ℚ))
Assuming n is a multiple of 4, the sensitivity of nisanExample
is n/2, achieved by any x with Hamming weight n/2.
@[category test, AMS 68]
lemma nisanExample_sensitivity (n : ℕ) (hn : 4 ∣ n) :
sensitivity (nisanExample n) = n / 2 := n:ℕhn:4 ∣ n⊢ sensitivity (nisanExample n) = n / 2
All goals completed! 🐙
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.
@[category test, AMS 68]
lemma nisanExample_blockSensitivity (n : ℕ) (hn : 4 ∣ n) :
blockSensitivity (nisanExample n) = 3 * n / 4 := n:ℕhn:4 ∣ n⊢ blockSensitivity (nisanExample n) = 3 * n / 4
All goals completed! 🐙
end Sensitivityend StrongSensitivityConjecture