Sensitivity, block sensitivity, and decision-tree lower bounds

The source separation is OpenAI's 2026 formalization: https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/lean/OAI/Combinatorics/Sensitivity/Separation.lean

Here sensitivity is the maximum number of sensitive coordinates at one input, not average sensitivity or Fourier total influence. Block sensitivity counts pairwise disjoint nonempty blocks whose flips change the output.

The source constructs finite nonconstant functions with block sensitivity larger than every constant multiple of squared sensitivity, and a family with a fixed power separation above exponent two. The decision-tree consequences below use complexitylib's existing DecisionTree.On model and its query depth. These are checked deductions; no claim is made that they were unknown to the source authors.

theorem Complexity.BooleanAnalysis.Sensitivity.sensitivityAt_le_blockSensitivityAt {I : Type} [Fintype I] (f : (I → Bool) → Bool) (x : I → Bool) : sensitivityAt f x ≤ blockSensitivityAt f x

Singleton blocks show that ordinary sensitivity never exceeds block sensitivity at an input.

theorem Complexity.BooleanAnalysis.Sensitivity.sensitivity_le_blockSensitivity {I : Type} [Fintype I] (f : (I → Bool) → Bool) : sensitivity f ≤ blockSensitivity f

Maximum sensitivity never exceeds maximum block sensitivity.

theorem Complexity.BooleanAnalysis.Sensitivity.exists_decisionTree {n : ℕ} (f : BitString n → Bool) : ∃ (tree : DecisionTree.On n), (∀ (x : BitString n), DecisionTree.On.eval x tree = f x) ∧ tree.depth ≤ n

Every finite Boolean function has an exact decision tree of depth at most its arity.

theorem Complexity.BooleanAnalysis.Sensitivity.blockSensitivity_le_depth {n : ℕ} (f : BitString n → Bool) (tree : DecisionTree.On n) (heval : ∀ (x : BitString n), DecisionTree.On.eval x tree = f x) : blockSensitivity f ≤ tree.depth

Every exact decision tree must query at least the block sensitivity in the worst case.

theorem Complexity.BooleanAnalysis.Sensitivity.blockSensitivity_le_arity {n : ℕ} (f : BitString n → Bool) : blockSensitivity f ≤ n

The block sensitivity of a Boolean function is at most its input arity.

theorem Complexity.BooleanAnalysis.Sensitivity.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) ≤ ↑(blockSensitivity f) / ↑(sensitivity f) ^ 2

OpenAI's quantitative superquadratic separation between block sensitivity and sensitivity.

theorem Complexity.BooleanAnalysis.Sensitivity.unbounded_quadratic_separation (C : ℝ) (hC : 0 < 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 < ↑(blockSensitivity f)

No constant multiple of squared sensitivity bounds block sensitivity for all Boolean functions.

theorem Complexity.BooleanAnalysis.Sensitivity.fixed_power_separation : ∃ (α : ℝ), 2 < α ∧ ∃ (n : ℕ → ℕ) (F : (m : ℕ) → (Fin (n m) → Bool) → Bool), (∀ (m : ℕ), 1 ≤ 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

OpenAI's fixed-power separation, with block sensitivity at zero tending to infinity.

theorem Complexity.BooleanAnalysis.Sensitivity.unbounded_quadratic_query_separation (C : ℝ) (hC : 0 < C) : ∃ (n : ℕ) (f : BitString n → Bool), 0 < n ∧ (f fun (x : Fin n) => false) = false ∧ (∃ (x : BitString n) (y : BitString n), f x ≠ f y) ∧ ∀ (tree : DecisionTree.On n), (∀ (x : BitString n), DecisionTree.On.eval x tree = f x) → C * ↑(sensitivity f) ^ 2 < ↑tree.depth

No constant multiple of squared sensitivity bounds the depth needed by exact decision trees.

theorem Complexity.BooleanAnalysis.Sensitivity.fixed_power_query_separation : ∃ (α : ℝ), 2 < α ∧ ∃ (n : ℕ → ℕ) (F : (m : ℕ) → BitString (n m) → Bool), (∀ (m : ℕ), 1 ≤ 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) ∧ ∀ (tree : DecisionTree.On (n m)), (∀ (x : BitString (n m)), DecisionTree.On.eval x tree = F m x) → ↑(sensitivity (F m)) ^ α ≤ ↑tree.depth) ∧ ∀ (trees : (m : ℕ) → DecisionTree.On (n m)), (∀ (m : ℕ) (x : BitString (n m)), DecisionTree.On.eval x (trees m) = F m x) → Filter.Tendsto (fun (m : ℕ) => ↑(trees m).depth) Filter.atTop Filter.atTop

A fixed exponent above two separates sensitivity from exact query depth. Every choice of exact trees for the family has unbounded depth.