Query-depth consequences of the sensitivity separation

Combine OpenAI's sensitivity separation with the canonical decision-tree bound blockSensitivity f ≤ tree.depth. These are deductions from the imported separation, without a claim of research novelty.

theorem Complexity.BooleanAnalysis.Sensitivity.Internal.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

theorem Complexity.BooleanAnalysis.Sensitivity.Internal.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