diff --git a/Cslib.lean b/Cslib.lean
index 6c20dd086..beaff4b59 100644
--- a/Cslib.lean
+++ b/Cslib.lean
@@ -64,6 +64,9 @@ public import Cslib.Computability.Machines.Turing.MultiTape.TapeLemmas
 public import Cslib.Computability.Machines.Turing.SingleTape.Defs
 public import Cslib.Computability.Machines.Turing.SingleTape.Deterministic
 public import Cslib.Computability.Machines.Turing.SingleTape.NonDeterministic
+public import Cslib.Computability.QueryComplexity.DecisionTree
+public import Cslib.Computability.QueryComplexity.Defs
+public import Cslib.Computability.QueryComplexity.Measures
 public import Cslib.Computability.URM.Basic
 public import Cslib.Computability.URM.Computable
 public import Cslib.Computability.URM.Defs
diff --git a/Cslib/Computability/QueryComplexity/DecisionTree.lean b/Cslib/Computability/QueryComplexity/DecisionTree.lean
new file mode 100644
index 000000000..aedf22a1d
--- /dev/null
+++ b/Cslib/Computability/QueryComplexity/DecisionTree.lean
@@ -0,0 +1,320 @@
+/-
+Copyright (c) 2026 Vignesh Karri. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Vignesh Karri
+-/
+
+module
+
+public import Cslib.Computability.QueryComplexity.Measures
+public import Mathlib.Order.Lattice.Nat
+public import Mathlib.Order.ConditionallyCompleteLattice.Basic
+
+/-!
+# Decision trees and decision tree complexity
+
+A decision tree over `n` variables queries one coordinate at a time and branches on the answer,
+until it reaches a leaf holding an output bit. It computes `f : BoolFunc n` when every input
+reaches a leaf labelled `f x`.
+
+`D(f)`, the decision tree complexity, is the least depth of a tree computing `f`. This file
+proves `C(f) ≤ D(f)`: the set of queries made when evaluating an input forms a certificate for
+that input. Together with `Measures.lean` that gives the chain
+
+`s(f) ≤ bs(f) ≤ C(f) ≤ D(f) ≤ n`.
+
+## Main definitions
+
+- `DecisionTree`: a decision tree over `n` Boolean variables.
+- `DecisionTree.Computes`: when a tree computes a given Boolean function.
+- `DecisionTree.depth`, `DecisionTree.cost`: worst-case and per-input query counts.
+- `DecisionTree.complexity`: `D(f)`, the least depth of a tree computing `f`.
+- `DecisionTree.path`: the partial assignment recording the queries made on an input.
+
+## Main results
+
+- `DecisionTree.complexity_le_card`: `D(f) ≤ n`.
+- `DecisionTree.certificateComplexity_le_complexity`: `C(f) ≤ D(f)`.
+
+## References
+
+* [S. Arora, B. Barak, *Computational Complexity: A Modern Approach*][AroraBarak09],
+  Section 12.1 (Decision trees and decision tree complexity) and Section 12.2
+  (Certificate Complexity).
+* [H. Buhrman, R. de Wolf, *Complexity measures and decision tree complexity:
+  a survey*][BuhrmanDeWolf2002]
+-/
+
+@[expose] public section
+
+namespace Cslib.QueryComplexity
+
+variable {n : ℕ}
+
+/-! ## Decision trees -/
+
+/-- A decision tree over `n` Boolean variables: either a leaf holding the output
+bit, or a node querying one coordinate. The left child is taken when the answer is
+`false`, the right child when it is `true`. -/
+inductive DecisionTree (n : Nat) where
+  | leaf (output : Bool) : DecisionTree n
+  | node (i : Fin n) : DecisionTree n → DecisionTree n → DecisionTree n
+
+namespace DecisionTree
+
+/-! ## Evaluation -/
+
+/-- Runs the input `x` through the decision tree and outputs the value at the leaf.
+The left child is the `false` branch, the right child the `true` branch. -/
+def eval : DecisionTree n → Cube n → Bool
+  | .leaf b, _ => b
+  | .node i l r, x => if x i then r.eval x else l.eval x
+
+/-- Decision Tree t computes f if for all inputs evaluating x on t gives the
+correct function value. -/
+def Computes (t : DecisionTree n) (f : BoolFunc n) : Prop :=
+  ∀ x, t.eval x = f x
+
+instance instDecidableComputes (t : DecisionTree n) (f : BoolFunc n) :
+    Decidable (t.Computes f) := inferInstanceAs (Decidable (∀ x, t.eval x = f x))
+
+/-- The depth of a tree: the number of queries on its longest root-to-leaf
+path. A leaf queries nothing, so it has depth `0`. -/
+def depth : DecisionTree n → ℕ
+  | .leaf _ => 0
+  | .node _ l r => max l.depth r.depth + 1
+
+@[simp]
+lemma depth_leaf (b : Bool) : (leaf b : DecisionTree n).depth = 0 := rfl
+
+/-- A node costs one query above its deeper child. -/
+@[simp]
+lemma depth_node (i : Fin n) (l r : DecisionTree n) :
+    (node i l r).depth = max l.depth r.depth + 1 := rfl
+
+/-! ## Paths
+
+The queries and answers along the route an input takes, as an `Assignment n`.
+This is used later when we prove that the path an input takes from route to
+leaf if a valid certificate for it.
+-/
+
+/-- The cost of running `t` on `x`: the number of queries actually made, i.e.
+the length of the single root-to-leaf path that `x` follows. -/
+def cost : DecisionTree n → Cube n → ℕ
+  | .leaf _, _ => 0
+  | .node i l r, x => (if x i then r.cost x else l.cost x) + 1
+
+@[simp]
+lemma cost_leaf (b : Bool) (x : Cube n) : (leaf b : DecisionTree n).cost x = 0 := rfl
+
+/-- A node charges one query, then continues into the child `x` selects. -/
+@[simp]
+lemma cost_node (i : Fin n) (l r : DecisionTree n) (x : Cube n) :
+    (node i l r).cost x = (if x i then r.cost x else l.cost x) + 1 := rfl
+
+/-- The route one input takes is no longer than the longest route in the tree. -/
+theorem cost_le_depth (t : DecisionTree n) (x : Cube n) : cost t x ≤ depth t := by
+  induction t with
+  | leaf out => simp
+  | node i l r l_ih r_ih =>
+    by_cases h : x i
+    · -- `x i` is true, so both `cost` and `eval` descend the RIGHT child
+      simp only [cost_node, h, ↓reduceIte, depth_node, add_le_add_iff_right, le_sup_iff]
+      exact Or.inr r_ih
+    · simp_all
+
+/-! ## The brute-force tree
+
+Every `f` is computed by some tree: one that queries every coordinate and
+then reads off the answer. This proves the set in the `complexity` definition is nonempty.
+-/
+
+/-- Query each coordinate of `is` in turn, then answer `f` on the accumulated
+input. `acc` records the answers so far; coordinates not yet queried keep whatever
+value `acc` came in with. -/
+def bruteForce (f : BoolFunc n) : List (Fin n) → Cube n → DecisionTree n
+  | [], acc => .leaf (f acc)
+  | i :: is, acc =>
+    .node i (bruteForce f is (Function.update acc i false))
+    (bruteForce f is (Function.update acc i true))
+
+/-- The tree asks exactly one question per coordinate of `is`. -/
+theorem depth_bruteForce (is : List (Fin n)) (acc : Cube n) (f : BoolFunc n) :
+    (bruteForce f is acc).depth = is.length := by
+  induction is generalizing acc with
+  | nil => simp [bruteForce]
+  | cons head tail tail_ih =>
+    simp [bruteForce, tail_ih]
+
+/-- Correctness in the generalized form. -/
+theorem eval_bruteForce (is : List (Fin n)) (acc : Cube n) (f : BoolFunc n) (x : Cube n)
+    (h : ∀ j, j ∉ is → x j = acc j) : (bruteForce f is acc).eval x = f x := by
+  induction is generalizing acc with
+  | nil =>
+    have hacc : acc = x := by grind
+    simp [bruteForce, eval, hacc]
+  | cons i is ih =>
+    have key : ∀ b : Bool, x i = b →
+        (bruteForce f is (Function.update acc i b)).eval x = f x := by
+      intro b hb
+      refine ih _ fun j hj => ?_
+      by_cases hji : j = i
+      · subst hji; simp [hb]
+      · rw [Function.update_of_ne hji]
+        exact h j (by simp [hji, hj])
+    simp only [bruteForce, eval]
+    by_cases hxi : x i = true
+    · simp [hxi, key true hxi]
+    · simp only [Bool.not_eq_true] at hxi
+      simp [hxi, key false hxi]
+
+/-- The brute-force tree for `f`: query every coordinate, in the order given by
+`List.finRange n`. -/
+def fullTree (f : BoolFunc n) : DecisionTree n := bruteForce f (List.finRange n) (fun _ => false)
+
+/-- Every function is computed by some tree. -/
+theorem fullTree_computes (f : BoolFunc n) : (fullTree f).Computes f := by
+  intro x
+  apply eval_bruteForce
+  simp
+
+/-- The depth of this brute force tree is `n`. -/
+@[simp]
+theorem depth_fullTree (f : BoolFunc n) : (fullTree f).depth = n := by
+  unfold fullTree
+  simp [depth_bruteForce]
+
+/-- `D(f)`: the least depth over all decision trees computing f. -/
+noncomputable def complexity (f : BoolFunc n) : ℕ :=
+  sInf {k | ∃ t : DecisionTree n, t.Computes f ∧ t.depth = k}
+
+/-- Upper-bound rule for `D(f)`. -/
+theorem complexity_le_depth {t : DecisionTree n} {f : BoolFunc n} (h : t.Computes f) :
+  complexity f ≤ t.depth := by
+  apply Nat.sInf_le
+  exact ⟨t, h, rfl⟩
+
+/-- The set of achievable depths is non-empty. -/
+theorem depths_nonempty (f : BoolFunc n) :
+    {k | ∃ t : DecisionTree n, t.Computes f ∧ t.depth = k}.Nonempty :=
+  ⟨n, fullTree f, fullTree_computes f, depth_fullTree f⟩
+
+/-- `D(f) ≤ n`: querying everything is always an option. -/
+theorem complexity_le_card (f : BoolFunc n) : complexity f ≤ n :=
+  (complexity_le_depth (fullTree_computes f)).trans_eq (depth_fullTree f)
+
+/-- An optimal tree exists. This follows from `Nat.sInf_mem`. -/
+theorem exists_computes_depth_eq_complexity (f : BoolFunc n) :
+    ∃ t : DecisionTree n, t.Computes f ∧ t.depth = complexity f :=
+  Nat.sInf_mem (depths_nonempty f)
+
+theorem le_complexity {f : BoolFunc n} {k : ℕ}
+    (h : ∀ t : DecisionTree n, t.Computes f → k ≤ t.depth) : k ≤ complexity f :=
+  le_csInf (depths_nonempty f) fun _ hb => by
+    obtain ⟨t, ht, rfl⟩ := hb
+    exact h t ht
+
+/-- The path of `x` through `t` is the partial assignment recording every query
+made along the route `x` takes, together with the answer given. -/
+def path : DecisionTree n → Cube n → Assignment n
+  | .leaf _, _ => fun _ => none
+  | .node i l r, x =>
+    if x i then Function.update (path r x) i (x i) else Function.update (path l x) i (x i)
+
+/-- The path partial assignment of x agrees with x. -/
+theorem agrees_path {t : DecisionTree n} {x : Cube n} : Agrees (path t x) x := by
+  induction t with
+  | leaf _ => simp [Agrees, path]
+  | node j l r l_ih r_ih =>
+    intro i b hb
+    simp only [path] at hb
+    rcases eq_or_ne i j with rfl | hij
+    · split at hb <;> simpa using hb
+    · split at hb
+      · exact r_ih i b (by rwa [Function.update_of_ne hij] at hb)
+      · exact l_ih i b (by rwa [Function.update_of_ne hij] at hb)
+
+lemma agrees_of_agrees_update {C : Assignment n} {x y : Cube n} {j : Fin n}
+    (hC : Agrees C x) (h : Agrees (Function.update C j (some (x j))) y) : Agrees C y := by
+  intro k c hk
+  rcases eq_or_ne k j with rfl | hkj
+  · have hy : y k = x k := h k (x k) (by simp)
+    rw [hy, hC k c hk]
+  · exact h k c (by rwa [Function.update_of_ne hkj])
+
+/-- If y agrees with the path partial assignment of x, then they both follow the
+same route from root to leaf. -/
+theorem routing {t : DecisionTree n} {x : Cube n} {y : Cube n} :
+    Agrees (path t x) y → t.eval y = t.eval x := by
+  induction t with
+  | leaf _ => simp [Agrees, path, eval]
+  | node j l r l_ih r_ih =>
+    intro h
+    -- the queried coordinate is recorded, so `y` must answer it exactly as `x` did
+    have hj : y j = x j := h j (x j) (by simp only [path]; split <;> simp)
+    simp only [path] at h
+    -- hence `y` takes the same branch, and the IH handles the subtree
+    simp only [eval, hj]
+    by_cases hxj : x j = true
+    · rw [ite_eq_left hxj] at h
+      simp only [ite_eq_left hxj]
+      exact r_ih (agrees_of_agrees_update agrees_path h)
+    · rw [ite_eq_right hxj] at h
+      simp only [ite_eq_right hxj]
+      exact l_ih (agrees_of_agrees_update agrees_path h)
+
+/-- Recording one more query enlarges the support by at most one coordinate. -/
+lemma support_update_subset (C : Assignment n) (j : Fin n) (b : Bool) :
+    support (Function.update C j (some b)) ⊆ insert j (support C) := by
+  intro i hi
+  rcases eq_or_ne i j with rfl | hij
+  · exact Finset.mem_insert_self _ _
+  · rw [mem_support, Function.update_of_ne hij] at hi
+    exact Finset.mem_insert_of_mem (mem_support.mpr hi)
+
+/-- The size of the path is at most the number of queries made. The inequality is not
+strict because making duplicate queries is allowed. -/
+theorem size_path_le_cost (t : DecisionTree n) (x : Cube n) : size (path t x) ≤ cost t x := by
+  induction t with
+  | leaf b => simp [path, size, support]
+  | node j l r l_ih r_ih =>
+    simp only [path, cost]
+    by_cases hxj : x j = true
+    · simp only [ite_eq_left hxj]
+      calc size (Function.update (path r x) j (some (x j)))
+          ≤ (insert j (support (path r x))).card :=
+            Finset.card_le_card (support_update_subset _ _ _)
+        _ ≤ (support (path r x)).card + 1 := Finset.card_insert_le _ _
+        _ ≤ cost r x + 1 := Nat.add_le_add_right r_ih 1
+    · simp only [ite_eq_right hxj]
+      calc size (Function.update (path l x) j (some (x j)))
+          ≤ (insert j (support (path l x))).card :=
+            Finset.card_le_card (support_update_subset _ _ _)
+        _ ≤ (support (path l x)).card + 1 := Finset.card_insert_le _ _
+        _ ≤ cost l x + 1 := Nat.add_le_add_right l_ih 1
+
+/-- The path is a certificate. -/
+theorem path_mem_certificates {f : BoolFunc n} {t : DecisionTree n} (ht : t.Computes f)
+    (x : Cube n) : path t x ∈ certificates f x :=
+  mem_certificates.mpr ⟨agrees_path, fun y hy => (ht y).symm.trans ((routing hy).trans (ht x))⟩
+
+/-- Pointwise: `Cₓ(f) ≤ D(f)`, by running the chain
+`Cₓ(f) ≤ size (path t x) ≤ cost t x ≤ depth t` over every tree computing `f`. -/
+theorem pointCertificateComplexity_le_complexity (f : BoolFunc n) (x : Cube n) :
+    pointCertificateComplexity f x ≤ complexity f := by
+  apply le_complexity
+  intro t ht
+  calc pointCertificateComplexity f x
+      ≤ size (path t x) := pointCertificateComplexity_le (path_mem_certificates ht x)
+    _ ≤ cost t x := size_path_le_cost t x
+    _ ≤ t.depth := cost_le_depth t x
+
+/-- `C(f) ≤ D(f)`. -/
+theorem certificateComplexity_le_complexity (f : BoolFunc n) :
+    certificateComplexity f ≤ complexity f :=
+  Finset.sup_le fun x _ => pointCertificateComplexity_le_complexity f x
+
+end DecisionTree
+
+end Cslib.QueryComplexity
diff --git a/Cslib/Computability/QueryComplexity/Defs.lean b/Cslib/Computability/QueryComplexity/Defs.lean
new file mode 100644
index 000000000..04ec8b074
--- /dev/null
+++ b/Cslib/Computability/QueryComplexity/Defs.lean
@@ -0,0 +1,130 @@
+/-
+Copyright (c) 2026 Vignesh Karri. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Vignesh Karri
+-/
+
+module
+
+public import Cslib.Init
+public import Mathlib.Data.Fintype.Card
+
+/-!
+# Boolean functions on the hypercube
+
+A Boolean function is a map `{0,1}ⁿ → {0,1}`. This file sets up the boolean hypercube, bit and block
+flips, and partial assignments. The complexity measures are built in
+`Measures.lean` and `DecisionTree.lean`.
+
+## Main definitions
+
+- `Cube n`: bit strings of length `n`, i.e. `Fin n → Bool`.
+- `BoolFunc n`: Boolean functions `Cube n → Bool`.
+- `Block n`: a set of coordinates.
+- `flipBit`, `flipBlock`: flipping one coordinate, or every coordinate of a block.
+- `PartialAssignment n`: a partial assignment, fixing some coordinates and leaving others free.
+- `Agrees`: An input is consistent with a partial assignment.
+
+## References
+
+* [S. Arora, B. Barak, *Computational Complexity: A Modern Approach*][AroraBarak09],
+  Chapter 12 (Decision Trees); the notions defined here underpin Sections 12.2 and 12.5.1.
+* [H. Buhrman, R. de Wolf, *Complexity measures and decision tree complexity:
+  a survey*][BuhrmanDeWolf2002]
+-/
+
+@[expose] public section
+
+namespace Cslib.QueryComplexity
+
+variable {n : ℕ}
+
+/-- Bit string of length `n`. -/
+abbrev Cube (n : ℕ) : Type := Fin n → Bool
+
+/-- `f : {0,1}ⁿ → {0,1}`. -/
+abbrev BoolFunc (n : ℕ) : Type := Cube n → Bool
+
+/-- A block: a set of coordinates. -/
+abbrev Block (n : ℕ) : Type := Finset (Fin n)
+
+/-- `x` with coordinate `i` flipped. Phrased with `Function.update` so that the
+whole `Function.update` simp set (`update_self`, `update_of_ne`, `update_idem`,
+`update_eq_self`, …) applies to it. -/
+def flipBit (x : Cube n) (i : Fin n) : Cube n := Function.update x i (!x i)
+
+/-- `x` with every coordinate of `B` flipped. -/
+def flipBlock (x : Cube n) (B : Block n) : Cube n :=
+  fun j => if j ∈ B then !(x j) else x j
+
+/-! ## Flipping lemmas -/
+
+/-- Flipping the same bit twice does nothing. -/
+@[simp]
+lemma flipBit_flipBit (x : Cube n) (i : Fin n) : flipBit (flipBit x i) i = x := by
+  simp [flipBit]
+
+/-- Flipping no coordinates does nothing. -/
+@[simp]
+lemma flipBlock_empty (x : Cube n) : flipBlock x ∅ = x := by
+  funext j; simp [flipBlock]
+
+/-- Flipping a block is an involution. -/
+@[simp]
+lemma flipBlock_flipBlock (x : Cube n) (B : Block n) :
+    flipBlock (flipBlock x B) B = x := by
+  funext j; by_cases h : j ∈ B <;> simp [flipBlock, h]
+
+/-- Flipping the block `{i}` is flipping the single bit `i`. -/
+@[simp]
+lemma flipBlock_singleton (x : Cube n) (i : Fin n) :
+    flipBlock x {i} = flipBit x i := by
+  funext j; by_cases h : j = i <;> simp [flipBlock, flipBit, h]
+
+/-- Flipping `B` then flipping `i ∈ B` back is flipping `B \ {i}`. -/
+lemma flipBlock_erase (x : Cube n) (B : Block n) {i : Fin n} (hi : i ∈ B) :
+    flipBlock x (B.erase i) = flipBit (flipBlock x B) i := by
+  funext j
+  by_cases hij : j = i
+  · subst hij; simp [flipBlock, flipBit, hi]
+  · simp [flipBit, flipBlock, hij]
+
+/-! ## Partial assignments -/
+
+/-- `C i = some b` fixes coordinate `i` to `b`; `C i = none` leaves it free. -/
+abbrev PartialAssignment (n : ℕ) : Type := Fin n → Option Bool
+
+/-- The coordinates the partial assignment fixes. -/
+def support (C : PartialAssignment n) : Finset (Fin n) :=
+  Finset.univ.filter (fun i => (C i).isSome)
+
+/-- A coordinate lies in the support exactly when the partial assignment fixes it. -/
+@[simp]
+lemma mem_support {C : PartialAssignment n} {i : Fin n} :
+    i ∈ support C ↔ (C i).isSome := by simp [support]
+
+/-- How many coordinates the partial assignment fixes. -/
+def size (C : PartialAssignment n) : ℕ := (support C).card
+
+/-- `x` agrees with `C` when it matches `C` on every fixed coordinate. -/
+def Agrees (C : PartialAssignment n) (x : Cube n) : Prop := ∀ i b, C i = some b → x i = b
+
+instance (C : PartialAssignment n) (x : Cube n) : Decidable (Agrees C x) :=
+  inferInstanceAs (Decidable (∀ i b, C i = some b → x i = b))
+
+/-- The total assignment reading off every coordinate of `x`. -/
+def ofCube (x : Cube n) : PartialAssignment n := fun i => some (x i)
+
+/-- A total assignment read off `x` is agreed with by `x` alone. -/
+@[simp]
+theorem agrees_ofCube_iff {x y : Cube n} : Agrees (ofCube x) y ↔ y = x := by
+  constructor
+  · intro h; funext i; exact h i (x i) rfl
+  · rintro rfl i b hb; simpa [ofCube] using hb
+
+/-- Reading off the whole input fixes all `n` coordinates. -/
+@[simp]
+theorem size_ofCube (x : Cube n) : size (ofCube x) = n := by
+  simp [size, support, ofCube]
+
+end Cslib.QueryComplexity
diff --git a/Cslib/Computability/QueryComplexity/Measures.lean b/Cslib/Computability/QueryComplexity/Measures.lean
new file mode 100644
index 000000000..f4b38294f
--- /dev/null
+++ b/Cslib/Computability/QueryComplexity/Measures.lean
@@ -0,0 +1,315 @@
+/-
+Copyright (c) 2026 Vignesh Karri. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Vignesh Karri
+-/
+
+module
+
+public import Cslib.Computability.QueryComplexity.Defs
+public import Mathlib.Data.Fintype.Pi
+public import Mathlib.Data.Fintype.Powerset
+public import Mathlib.Data.Fintype.Option
+public import Mathlib.Data.Finset.Lattice.Fold
+public import Mathlib.Algebra.Order.BigOperators.Group.Finset
+
+/-!
+# Boolean function complexity measures
+
+Sensitivity `s(f)`, block sensitivity `bs(f)` and certificate complexity `C(f)`, together with
+the chain `s(f) ≤ bs(f) ≤ C(f)`. Notation follows [AroraBarak09].
+
+## Main definitions
+
+- `sensitivity`: `s(f)`, the maximum over inputs of the number of sensitive coordinates.
+- `blockSensitivity`: `bs(f)`, the maximum over inputs of the maximum number of disjoint sensitive
+  blocks.
+- `certificateComplexity`: `C(f)`, the maximum over inputs of the smallest certificate size.
+
+## Main results
+
+- `sensitivity_le_blockSensitivity`: `s(f) ≤ bs(f)`.
+- `blockSensitivity_le_certificateComplexity`: `bs(f) ≤ C(f)`.
+- `|B| ≤ s(f)` for a minimal sensitive block `B`.
+
+## References
+
+* [S. Arora, B. Barak, *Computational Complexity: A Modern Approach*][AroraBarak09],
+  Section 12.2 (Certificate Complexity) and Section 12.5.1 (Sensitivity).
+* [H. Buhrman, R. de Wolf, *Complexity measures and decision tree complexity:
+  a survey*][BuhrmanDeWolf2002]
+-/
+
+@[expose] public section
+
+namespace Cslib.QueryComplexity
+
+variable {n : ℕ}
+
+/-! ## Sensitivity -/
+
+/-- Coordinate `i` is sensitive for `f` at `x` when flipping it flips `f`. -/
+def IsSensitiveCoord (f : BoolFunc n) (x : Cube n) (i : Fin n) : Prop :=
+  f (flipBit x i) ≠ f x
+
+instance (f : BoolFunc n) (x : Cube n) : DecidablePred (IsSensitiveCoord f x) :=
+  fun i => inferInstanceAs (Decidable (f (flipBit x i) ≠ f x))
+
+/-- The set of coordinates sensitive for `f` at `x`. -/
+def sensitiveCoords (f : BoolFunc n) (x : Cube n) : Finset (Fin n) :=
+  Finset.univ.filter (IsSensitiveCoord f x)
+
+/-- The bridge between the predicate and the `Finset` it cuts out. -/
+@[simp]
+lemma mem_sensitiveCoords {f : BoolFunc n} {x : Cube n} {i : Fin n} :
+    i ∈ sensitiveCoords f x ↔ IsSensitiveCoord f x i := by
+  simp [sensitiveCoords]
+
+/-- The number of sensitive coordinates in input `x`, usually denoted `sₓ(f)`. -/
+def pointSensitivity (f : BoolFunc n) (x : Cube n) : ℕ := (sensitiveCoords f x).card
+
+/-- The maximum sensitivity over all inputs, denoted `s(f)`. -/
+def sensitivity (f : BoolFunc n) : ℕ := Finset.univ.sup (pointSensitivity f)
+
+/-- Lower-bound rule for `sₓ(f)`: exhibit a set of sensitive coordinates. -/
+lemma card_le_pointSensitivity {f : BoolFunc n} {x : Cube n} {S : Finset (Fin n)}
+    (h : ∀ i ∈ S, IsSensitiveCoord f x i) : S.card ≤ pointSensitivity f x := by
+  apply Finset.card_le_card
+  simpa [Finset.subset_iff] using h
+
+/-- The sensitivity at a single input is at most the sensitivity of `f`: `sₓ(f) ≤ s(f)`. -/
+lemma pointSensitivity_le_sensitivity (f : BoolFunc n) (x : Cube n) :
+    pointSensitivity f x ≤ sensitivity f :=
+  Finset.le_sup (Finset.mem_univ x)
+
+/-- Lower-bound rule for `s(f)`: sensitive coordinates at any input suffice. -/
+lemma card_le_sensitivity {f : BoolFunc n} {x : Cube n} {S : Finset (Fin n)}
+    (h : ∀ i ∈ S, IsSensitiveCoord f x i) : S.card ≤ sensitivity f :=
+  (card_le_pointSensitivity h).trans (pointSensitivity_le_sensitivity f x)
+
+/-! ## Block sensitivity -/
+
+/-- Block `B` is sensitive for `f` at `x` when flipping all bits of `B` flips `f`. -/
+def IsSensitiveBlock (f : BoolFunc n) (x : Cube n) (B : Block n) : Prop :=
+  f (flipBlock x B) ≠ f x
+
+instance (f : BoolFunc n) (x : Cube n) (B : Block n) : Decidable (IsSensitiveBlock f x B) :=
+  inferInstanceAs (Decidable (f (flipBlock x B) ≠ f x))
+
+/-- Every member flips `f`, and the members are pairwise disjoint. -/
+def IsSensitiveFamily (f : BoolFunc n) (x : Cube n) (F : Finset (Block n)) : Prop :=
+  (∀ B ∈ F, IsSensitiveBlock f x B) ∧ (F : Set (Block n)).PairwiseDisjoint id
+
+instance (f : BoolFunc n) (x : Cube n) (F : Finset (Block n)) :
+    Decidable (IsSensitiveFamily f x F) :=
+  decidable_of_iff ((∀ B ∈ F, IsSensitiveBlock f x B) ∧
+    ∀ P ∈ F, ∀ Q ∈ F, P ≠ Q → Disjoint P Q) Iff.rfl
+
+/-- All sensitive families. -/
+def sensitiveFamilies (f : BoolFunc n) (x : Cube n) : Finset (Finset (Block n)) :=
+  Finset.univ.filter (IsSensitiveFamily f x)
+
+@[simp]
+lemma mem_sensitiveFamilies {f : BoolFunc n} {x : Cube n} {F : Finset (Block n)} :
+    F ∈ sensitiveFamilies f x ↔ IsSensitiveFamily f x F := by
+  simp [sensitiveFamilies]
+
+/-- The block sensitivity of `f` at `x`: the largest number of pairwise disjoint blocks of
+coordinates such that flipping every coordinate of any one block flips `f`. Usually denoted
+`bsₓ(f)`. -/
+def pointBlockSensitivity (f : BoolFunc n) (x : Cube n) : ℕ :=
+  (sensitiveFamilies f x).sup Finset.card
+
+/-- The maximum block sensitivity over all inputs, denoted `bs(f)`. -/
+def blockSensitivity (f : BoolFunc n) : ℕ := Finset.univ.sup (pointBlockSensitivity f)
+
+/-- Lower-bound rule for `bsₓ(f)`: exhibit one sensitive family. -/
+lemma card_le_pointBlockSensitivity {f : BoolFunc n} {x : Cube n} {F : Finset (Block n)}
+    (h : IsSensitiveFamily f x F) : F.card ≤ pointBlockSensitivity f x :=
+  Finset.le_sup (mem_sensitiveFamilies.mpr h)
+
+/-- The block sensitivity at a single input is at most that of `f`: `bsₓ(f) ≤ bs(f)`. -/
+lemma pointBlockSensitivity_le_blockSensitivity (f : BoolFunc n) (x : Cube n) :
+    pointBlockSensitivity f x ≤ blockSensitivity f :=
+  Finset.le_sup (Finset.mem_univ x)
+
+/-- Lower-bound rule for `bs(f)`. -/
+lemma card_le_blockSensitivity {f : BoolFunc n} {x : Cube n} {F : Finset (Block n)}
+    (h : IsSensitiveFamily f x F) : F.card ≤ blockSensitivity f :=
+  (card_le_pointBlockSensitivity h).trans (pointBlockSensitivity_le_blockSensitivity f x)
+
+/-! ## Sensitive singletons -/
+
+/-- A singleton block is sensitive exactly when its coordinate is. -/
+@[simp]
+lemma isSensitiveBlock_singleton {f : BoolFunc n} {x : Cube n} {i : Fin n} :
+    IsSensitiveBlock f x {i} ↔ IsSensitiveCoord f x i := by
+  rw [IsSensitiveBlock, IsSensitiveCoord, flipBlock_singleton]
+
+/-! ## `s(f) ≤ bs(f)` -/
+
+/-- One block per sensitive coordinate. -/
+def singletonFamily (f : BoolFunc n) (x : Cube n) : Finset (Block n) :=
+  (sensitiveCoords f x).image (fun i => ({i} : Block n))
+
+/-- Membership in the singleton family: one block per sensitive coordinate. -/
+@[simp]
+lemma mem_singletonFamily {f : BoolFunc n} {x : Cube n} {B : Block n} :
+    B ∈ singletonFamily f x ↔ ∃ i, IsSensitiveCoord f x i ∧ {i} = B := by
+  simp [singletonFamily]
+
+/-- The singleton family has one block per sensitive coordinate, so `sₓ(f)` of them. -/
+@[simp]
+lemma card_singletonFamily {f : BoolFunc n} {x : Cube n} :
+    (singletonFamily f x).card = pointSensitivity f x :=
+  Finset.card_image_of_injective _ Finset.singleton_injective
+
+/-- Singletons of distinct sensitive coordinates do form a sensitive family: each
+flips `f`, and distinct singletons are disjoint. -/
+lemma isSensitiveFamily_singletonFamily {f : BoolFunc n} {x : Cube n} :
+    IsSensitiveFamily f x (singletonFamily f x) := by
+  constructor
+  · rintro B hB
+    obtain ⟨i, hi, rfl⟩ := mem_singletonFamily.mp hB
+    exact isSensitiveBlock_singleton.mpr hi
+  · rintro P hP Q hQ hPQ
+    obtain ⟨i, -, rfl⟩ := mem_singletonFamily.mp hP
+    obtain ⟨j, -, rfl⟩ := mem_singletonFamily.mp hQ
+    exact Finset.disjoint_singleton.mpr fun h => hPQ (by rw [h])
+
+/-- Pointwise: `sₓ(f) ≤ bsₓ(f)`. -/
+theorem pointSensitivity_le_pointBlockSensitivity (f : BoolFunc n) (x : Cube n) :
+    pointSensitivity f x ≤ pointBlockSensitivity f x :=
+  card_singletonFamily ▸ card_le_pointBlockSensitivity isSensitiveFamily_singletonFamily
+
+/-- Every sensitive coordinate is a sensitive block of size one, so `s(f) ≤ bs(f)`. -/
+theorem sensitivity_le_blockSensitivity (f : BoolFunc n) :
+    sensitivity f ≤ blockSensitivity f :=
+  Finset.sup_mono_fun fun x _ => pointSensitivity_le_pointBlockSensitivity f x
+
+/-! ## Minimal sensitive blocks -/
+
+/-- `B` is sensitive, and no proper subset of `B` is sensitive. -/
+def IsMinimalSensitiveBlock (f : BoolFunc n) (x : Cube n) (B : Block n) : Prop :=
+  IsSensitiveBlock f x B ∧ ∀ C ⊂ B, ¬ IsSensitiveBlock f x C
+
+instance (f : BoolFunc n) (x : Cube n) (B : Block n) :
+    Decidable (IsMinimalSensitiveBlock f x B) :=
+  inferInstanceAs (Decidable (IsSensitiveBlock f x B ∧ ∀ C ⊂ B, ¬ IsSensitiveBlock f x C))
+
+namespace IsMinimalSensitiveBlock
+
+variable {f : BoolFunc n} {x : Cube n} {B : Block n} {i : Fin n}
+
+/-- Dropping any coordinate from a minimal sensitive block breaks sensitivity. -/
+lemma not_isSensitiveBlock_erase (hB : IsMinimalSensitiveBlock f x B) (hi : i ∈ B) :
+    ¬ IsSensitiveBlock f x (B.erase i) :=
+  hB.2 _ (Finset.erase_ssubset hi)
+
+/-- Every coordinate of a minimal sensitive block is sensitive at the input which
+has the minimal sensitive block flipped. -/
+lemma isSensitiveCoord_flipBlock (hB : IsMinimalSensitiveBlock f x B) (hi : i ∈ B) :
+    IsSensitiveCoord f (flipBlock x B) i := by
+  unfold IsSensitiveCoord
+  rw [← flipBlock_erase x B hi, not_not.mp (hB.not_isSensitiveBlock_erase hi)]
+  exact Ne.symm hB.1
+
+/-- `|B| ≤ s(f)` for a minimal sensitive block `B`. -/
+theorem card_le_sensitivity (hB : IsMinimalSensitiveBlock f x B) : B.card ≤ sensitivity f :=
+  _root_.Cslib.QueryComplexity.card_le_sensitivity fun _ hi => hB.isSensitiveCoord_flipBlock hi
+
+end IsMinimalSensitiveBlock
+
+/-! ## Certificates -/
+
+/-- `C` forces the value `b`: everything consistent with `C` has `f = b`. -/
+def IsCertificate (f : BoolFunc n) (C : PartialAssignment n) (b : Bool) : Prop :=
+  ∀ x, Agrees C x → f x = b
+
+instance (f : BoolFunc n) (C : PartialAssignment n) (b : Bool) : Decidable (IsCertificate f C b) :=
+  inferInstanceAs (Decidable (∀ x, Agrees C x → f x = b))
+
+/-- Assignments consistent with `x` that already force `f x`. -/
+def certificates (f : BoolFunc n) (x : Cube n) : Finset (PartialAssignment n) :=
+  Finset.univ.filter (fun C => Agrees C x ∧ IsCertificate f C (f x))
+
+@[simp]
+lemma mem_certificates {f : BoolFunc n} {x : Cube n} {C : PartialAssignment n} :
+    C ∈ certificates f x ↔ Agrees C x ∧ IsCertificate f C (f x) := by
+  simp [certificates]
+
+/-- Reading off all of `x` is always a certificate. -/
+lemma ofCube_mem_certificates (f : BoolFunc n) (x : Cube n) : ofCube x ∈ certificates f x :=
+  mem_certificates.mpr ⟨agrees_ofCube_iff.mpr rfl, fun _ hy => by
+    rw [agrees_ofCube_iff.mp hy]⟩
+
+/-- There is always a certificate, so `Cₓ(f)` is a minimum over a non-empty set. -/
+lemma certificates_nonempty (f : BoolFunc n) (x : Cube n) : (certificates f x).Nonempty :=
+  ⟨ofCube x, ofCube_mem_certificates f x⟩
+
+/-- The size of the smallest certificate for the input `x`, denoted `Cₓ(f)`. -/
+def pointCertificateComplexity (f : BoolFunc n) (x : Cube n) : ℕ :=
+  (certificates f x).inf' (certificates_nonempty f x) size
+
+/-- Upper-bound rule for `Cₓ(f)`: exhibit one certificate. -/
+lemma pointCertificateComplexity_le {f : BoolFunc n} {x : Cube n} {C : PartialAssignment n}
+    (h : C ∈ certificates f x) : pointCertificateComplexity f x ≤ size C :=
+  Finset.inf'_le _ h
+
+/-- The maximum over all inputs of the smallest certificate size, denoted `C(f)`. -/
+def certificateComplexity (f : BoolFunc n) : ℕ :=
+  Finset.univ.sup (pointCertificateComplexity f)
+
+/-- The certificate complexity at a single input is at most that of `f`: `Cₓ(f) ≤ C(f)`. -/
+lemma pointCertificateComplexity_le_certificateComplexity (f : BoolFunc n) (x : Cube n) :
+    pointCertificateComplexity f x ≤ certificateComplexity f :=
+  Finset.le_sup (Finset.mem_univ x)
+
+/-- `Cₓ(f) ≤ n`: reading off the whole input is a certificate. -/
+theorem pointCertificateComplexity_le_card (f : BoolFunc n) (x : Cube n) :
+    pointCertificateComplexity f x ≤ n :=
+  (pointCertificateComplexity_le (ofCube_mem_certificates f x)).trans_eq (size_ofCube x)
+
+/-! ## `bs(f) ≤ C(f)`
+
+A valid certificate for x must contain at least one bit from every block in a
+sensitive family.
+-/
+
+/-- A certificate must fix at least one coordinate of every sensitive block. -/
+theorem sensitiveBlock_inter_support_nonempty {f : BoolFunc n} (x : Cube n) (B : Block n)
+    (hB : IsSensitiveBlock f x B) (C : PartialAssignment n) (hC : C ∈ certificates f x) :
+    (B ∩ support C).Nonempty := by
+  obtain ⟨hAgr, hCert⟩ := mem_certificates.mp hC
+  by_contra h
+  rw [Finset.not_nonempty_iff_eq_empty, Finset.eq_empty_iff_forall_notMem] at h
+  refine hB (hCert _ fun i b hb => ?_)
+  have hi : i ∉ B := fun hiB =>
+    h i (Finset.mem_inter.mpr ⟨hiB, mem_support.mpr (by simp [hb])⟩)
+  simpa [flipBlock, hi] using hAgr i b hb
+
+/-- A certificate is at least as large as any sensitive family. -/
+lemma card_le_size_of_isSensitiveFamily {f : BoolFunc n} {x : Cube n}
+    {F : Finset (Block n)} {C : PartialAssignment n}
+    (hF : IsSensitiveFamily f x F) (hC : C ∈ certificates f x) : F.card ≤ size C :=
+  (Finset.card_le_card_biUnion
+      (fun _ hP _ hQ hPQ => Disjoint.mono Finset.inter_subset_left Finset.inter_subset_left
+        (hF.2 hP hQ hPQ))
+      (fun B hB => sensitiveBlock_inter_support_nonempty x B (hF.1 B hB) C hC)).trans
+    (Finset.card_le_card (Finset.biUnion_subset.mpr fun _ _ => Finset.inter_subset_right))
+
+/-- Pointwise: `bsₓ(f) ≤ Cₓ(f)`. -/
+theorem pointBlockSensitivity_le_pointCertificateComplexity
+    (f : BoolFunc n) (x : Cube n) :
+    pointBlockSensitivity f x ≤ pointCertificateComplexity f x :=
+  Finset.sup_le fun _ hF => Finset.le_inf' _ _ fun _ hC =>
+    card_le_size_of_isSensitiveFamily (mem_sensitiveFamilies.mp hF) hC
+
+/-- Every block of a sensitive family meets the support of any certificate, so
+`bs(f) ≤ C(f)`. -/
+theorem blockSensitivity_le_certificateComplexity (f : BoolFunc n) :
+    blockSensitivity f ≤ certificateComplexity f :=
+  Finset.sup_mono_fun fun x _ =>
+    pointBlockSensitivity_le_pointCertificateComplexity f x
+
+end Cslib.QueryComplexity
diff --git a/CslibTests.lean b/CslibTests.lean
index 016de8648..b023a9794 100644
--- a/CslibTests.lean
+++ b/CslibTests.lean
@@ -23,5 +23,6 @@ import CslibTests.Modal.Ideal
 import CslibTests.Modal.Stlc
 import CslibTests.MultiTapeComplexity
 import CslibTests.PACLearning
+import CslibTests.QueryComplexity
 import CslibTests.Reduction
 import CslibTests.StatefulProcesses
diff --git a/CslibTests/QueryComplexity.lean b/CslibTests/QueryComplexity.lean
new file mode 100644
index 000000000..5d97a2ed8
--- /dev/null
+++ b/CslibTests/QueryComplexity.lean
@@ -0,0 +1,119 @@
+/-
+Copyright (c) 2026 Vignesh Karri. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Vignesh Karri
+-/
+
+import Cslib.Computability.QueryComplexity.Measures
+import Mathlib.Data.Fin.VecNotation
+
+/-! # Query complexity tests
+
+Worked examples of `s(f)`, `bs(f)`, `C(f)` and `D(f)` on some standard Boolean
+functions.
+
+`s`, `bs`, and `C` are all decidable and `D(f)` is not. We have proved the chain
+`s ≤ bs ≤ C ≤ D`.
+-/
+
+namespace CslibTests.QueryComplexity
+
+open Cslib.QueryComplexity
+
+/-! ## The functions -/
+
+/-- `OR` of `n` bits. -/
+def orF (n : ℕ) : BoolFunc n := fun x => (List.ofFn x).any id
+
+/-- `AND` of `n` bits. -/
+def andF (n : ℕ) : BoolFunc n := fun x => (List.ofFn x).all id
+
+/-- `PARITY` of `n` bits. -/
+def parityF (n : ℕ) : BoolFunc n := fun x => (List.ofFn x).foldr xor false
+
+/-- `MAJ` on three bits: at least two of the three inputs are `true`. -/
+def maj3 : BoolFunc 3 := fun x => (x 0 && x 1) || (x 1 && x 2) || (x 0 && x 2)
+
+example : orF 3 ![false, false, false] = false := rfl
+example : orF 3 ![false, true, false] = true := rfl
+example : andF 3 ![true, true, true] = true := rfl
+example : andF 3 ![true, false, true] = false := rfl
+example : parityF 3 ![true, true, true] = true := rfl
+example : parityF 3 ![true, true, false] = false := rfl
+example : maj3 ![true, true, false] = true := rfl
+example : maj3 ![true, false, false] = false := rfl
+
+/-! ## OR
+Every coordinate is sensitive at the all zeroes input, so `s=n`, hence
+`D=n` since `s(f) ≤ D(f)`. This also implies `OR` has all four measures equal to `n`.
+-/
+
+example : sensitivity (orF 2) = 2 := by decide
+example : blockSensitivity (orF 2) = 2 := by decide
+example : certificateComplexity (orF 2) = 2 := by decide
+
+example : sensitivity (orF 3) = 3 := by decide
+example : blockSensitivity (orF 3) = 3 := by decide
+example : certificateComplexity (orF 3) = 3 := by decide
+
+/-- A single `true` bit is a certificate for `OR`. -/
+example : pointCertificateComplexity (orF 3) ![true, true, true] = 1 := by decide
+
+/-- The size of the smallest certificate at the all zeroes input is the size of the
+whole string. -/
+example : pointCertificateComplexity (orF 3) ![false, false, false] = 3 := by decide
+
+/-! ## AND
+
+The all-`true` input is sensitive
+-/
+
+example : sensitivity (andF 3) = 3 := by decide
+example : blockSensitivity (andF 3) = 3 := by decide
+example : certificateComplexity (andF 3) = 3 := by decide
+
+/-! ## PARITY
+
+Every coordinate is sensitive at every input, which is the extreme case.
+-/
+
+example : sensitivity (parityF 2) = 2 := by decide
+example : blockSensitivity (parityF 2) = 2 := by decide
+example : certificateComplexity (parityF 2) = 2 := by decide
+
+example : sensitivity (parityF 3) = 3 := by decide
+example : blockSensitivity (parityF 3) = 3 := by decide
+example : certificateComplexity (parityF 3) = 3 := by decide
+
+/-- No short certificate at any input. -/
+example : pointCertificateComplexity (parityF 3) ![true, true, true] = 3 := by decide
+
+/-! ## MAJ₃
+
+Here the measures come apart: `s = bs = C = 2`, `D = 3`.
+-/
+
+example : sensitivity maj3 = 2 := by decide
+example : blockSensitivity maj3 = 2 := by decide
+example : certificateComplexity maj3 = 2 := by decide
+
+/-- An all-`true` has no sensitive bits. -/
+example : pointSensitivity maj3 ![true, true, true] = 0 := by decide
+
+/-- A split input is sensitive in the two agreeing coordinates, but not the third. -/
+example : sensitiveCoords maj3 ![true, true, false] = {0, 1} := by decide
+
+/-- Two agreeing bits are a certificate, so `Cₓ(f) = 2` everywhere. -/
+example : pointCertificateComplexity maj3 ![true, true, false] = 2 := by decide
+
+/-! ## Constant functions
+
+No bit is sensitive. The empty assignment is a certificate and the trivial tree computes
+the function.
+-/
+
+example : sensitivity (fun _ => true : BoolFunc 3) = 0 := by decide
+example : blockSensitivity (fun _ => true : BoolFunc 3) = 0 := by decide
+example : certificateComplexity (fun _ => true : BoolFunc 3) = 0 := by decide
+
+end CslibTests.QueryComplexity
diff --git a/references.bib b/references.bib
index 72051ea9c..1c3cbeefe 100644
--- a/references.bib
+++ b/references.bib
@@ -80,6 +80,16 @@ @misc{BonehShoup2023
   url          = {https://crypto.stanford.edu/~dabo/cryptobook/BonehShoup_0_6.pdf}
 }
 
+@article{BuhrmanDeWolf2002,
+  author  = {Buhrman, Harry and de Wolf, Ronald},
+  title   = {Complexity measures and decision tree complexity: a survey},
+  journal = {Theoretical Computer Science},
+  volume  = {288},
+  number  = {1},
+  pages   = {21--43},
+  year    = {2002}
+}
+
 @misc{Burghardt2018,
 	title = {Simple {Laws} about {Nonprominent} {Properties} of {Binary} {Relations}},
 	url = {https://arxiv.org/abs/1806.05036v2},