From 67f1befb7adaa9f4a3946bfcd989b6ba2ebdab1b Mon Sep 17 00:00:00 2001
From: Vignesh Karri <vigneshkarri5@gmail.com>
Date: Fri, 18 Sep 2026 21:52:32 +0530
Subject: [PATCH 1/7] feat(Complexity): Query Complexity of Boolean Functions
 (aka Decision Tree Complexity). Defines sensitivity, block sensitivity and
 certificate complexity.

---
 Cslib.lean                                    |   2 +
 Cslib/Computability/QueryComplexity/Defs.lean | 140 ++++++++
 .../QueryComplexity/Measures.lean             | 312 ++++++++++++++++++
 CslibTests.lean                               |   1 +
 CslibTests/QueryComplexity.lean               | 119 +++++++
 references.bib                                |  20 ++
 6 files changed, 594 insertions(+)
 create mode 100644 Cslib/Computability/QueryComplexity/Defs.lean
 create mode 100644 Cslib/Computability/QueryComplexity/Measures.lean
 create mode 100644 CslibTests/QueryComplexity.lean

diff --git a/Cslib.lean b/Cslib.lean
index 6c20dd086..34b090c71 100644
--- a/Cslib.lean
+++ b/Cslib.lean
@@ -64,6 +64,8 @@ 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.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/Defs.lean b/Cslib/Computability/QueryComplexity/Defs.lean
new file mode 100644
index 000000000..ae21027d3
--- /dev/null
+++ b/Cslib/Computability/QueryComplexity/Defs.lean
@@ -0,0 +1,140 @@
+/-
+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.
+- `Assignment 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*][AroraBarak2009],
+  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)
+
+/-- The flipped coordinate reads back negated. -/
+@[simp]
+lemma flipBit_self (x : Cube n) (i : Fin n) : flipBit x i i = !x i :=
+  Function.update_self ..
+
+/-- Every other coordinate is left alone. -/
+@[simp]
+lemma flipBit_of_ne {x : Cube n} {i j : Fin n} (h : j ≠ i) : flipBit x i j = x j :=
+  Function.update_of_ne h ..
+
+/-- `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 Assignment (n : ℕ) : Type := Fin n → Option Bool
+
+/-- The coordinates the assignment fixes. -/
+def support (C : Assignment n) : Finset (Fin n) :=
+  Finset.univ.filter (fun i => (C i).isSome)
+
+/-- A coordinate lies in the support exactly when the assignment fixes it. -/
+@[simp]
+lemma mem_support {C : Assignment n} {i : Fin n} :
+    i ∈ support C ↔ (C i).isSome := by simp [support]
+
+/-- How many coordinates the assignment fixes. -/
+def size (C : Assignment n) : ℕ := (support C).card
+
+/-- `x` agrees with `C` when it matches `C` on every fixed coordinate. -/
+def Agrees (C : Assignment n) (x : Cube n) : Prop := ∀ i b, C i = some b → x i = b
+
+instance (C : Assignment 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) : Assignment 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..d34ccf132
--- /dev/null
+++ b/Cslib/Computability/QueryComplexity/Measures.lean
@@ -0,0 +1,312 @@
+/-
+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)`.
+
+## 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*][AroraBarak2009],
+  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]
+
+/-- `s(f, x)` is the number of sensitive coordinates in input `x`. -/
+def pointSensitivity (f : BoolFunc n) (x : Cube n) : ℕ := (sensitiveCoords f x).card
+
+/-- `s(f)`. -/
+def sensitivity (f : BoolFunc n) : ℕ := Finset.univ.sup (pointSensitivity f)
+
+/-- Lower-bound rule for `s(f, x)`: 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
+
+/-- `s(f, x) ≤ 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]
+
+/-- `bs(f, x)`. -/
+def pointBlockSensitivity (f : BoolFunc n) (x : Cube n) : ℕ :=
+  (sensitiveFamilies f x).sup Finset.card
+
+/-- `bs(f)`. -/
+def blockSensitivity (f : BoolFunc n) : ℕ := Finset.univ.sup (pointBlockSensitivity f)
+
+/-- Lower-bound rule for `bs(f, x)`: 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)
+
+/-- `bs(f, x) ≤ 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, x)` 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, x) ≤ bs(f, x)`. -/
+theorem pointSensitivity_le_pointBlockSensitivity (f : BoolFunc n) (x : Cube n) :
+    pointSensitivity f x ≤ pointBlockSensitivity f x :=
+  card_singletonFamily ▸ card_le_pointBlockSensitivity isSensitiveFamily_singletonFamily
+
+/-- `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 : Assignment n) (b : Bool) : Prop :=
+  ∀ x, Agrees C x → f x = b
+
+instance (f : BoolFunc n) (C : Assignment 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 (Assignment 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 : Assignment 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, x)` 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⟩
+
+/-- `C(f, x)`: the size of the smallest certificate. -/
+def pointCertificateComplexity (f : BoolFunc n) (x : Cube n) : ℕ :=
+  (certificates f x).inf' (certificates_nonempty f x) size
+
+/-- Upper-bound rule for `C(f, x)`: exhibit one certificate. -/
+lemma pointCertificateComplexity_le {f : BoolFunc n} {x : Cube n} {C : Assignment n}
+    (h : C ∈ certificates f x) : pointCertificateComplexity f x ≤ size C :=
+  Finset.inf'_le _ h
+
+/-- `C(f)`. -/
+def certificateComplexity (f : BoolFunc n) : ℕ :=
+  Finset.univ.sup (pointCertificateComplexity f)
+
+/-- `C(f, x) ≤ 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, x) ≤ 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 : Assignment 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 : Assignment 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, x) ≤ C(f, x)`. -/
+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
+
+/-- `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..605b761c5
--- /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, x) = 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..96917c56c 100644
--- a/references.bib
+++ b/references.bib
@@ -53,6 +53,16 @@ @article{AngluinLaird1988
   doi          = {10.1007/BF00116829}
 }
 
+@book{AroraBarak2009,
+  author    = {Arora, Sanjeev and Barak, Boaz},
+  title     = {Computational Complexity: A Modern Approach},
+  year      = {2009},
+  isbn      = {9780521424264},
+  publisher = {Cambridge University Press},
+  address   = {New York},
+  url       = {https://theory.cs.princeton.edu/complexity/}
+}
+
 @book{Baader1998,
 author = {Baader, Franz and Nipkow, Tobias},
 title = {Term rewriting and all that},
@@ -80,6 +90,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},

From 2d67763fd60a17fd6679e8c47f769e877bef452c Mon Sep 17 00:00:00 2001
From: Vignesh Karri <vigneshkarri5@gmail.com>
Date: Fri, 18 Sep 2026 22:10:51 +0530
Subject: [PATCH 2/7] fix: use existing AroraBarak09 bib key

---
 Cslib/Computability/QueryComplexity/Defs.lean     |  2 +-
 Cslib/Computability/QueryComplexity/Measures.lean |  2 +-
 references.bib                                    | 10 ----------
 3 files changed, 2 insertions(+), 12 deletions(-)

diff --git a/Cslib/Computability/QueryComplexity/Defs.lean b/Cslib/Computability/QueryComplexity/Defs.lean
index ae21027d3..13a2fa93b 100644
--- a/Cslib/Computability/QueryComplexity/Defs.lean
+++ b/Cslib/Computability/QueryComplexity/Defs.lean
@@ -27,7 +27,7 @@ flips, and partial assignments. The complexity measures are built in
 
 ## References
 
-* [S. Arora, B. Barak, *Computational Complexity: A Modern Approach*][AroraBarak2009],
+* [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]
diff --git a/Cslib/Computability/QueryComplexity/Measures.lean b/Cslib/Computability/QueryComplexity/Measures.lean
index d34ccf132..2d55eecc9 100644
--- a/Cslib/Computability/QueryComplexity/Measures.lean
+++ b/Cslib/Computability/QueryComplexity/Measures.lean
@@ -34,7 +34,7 @@ the chain `s(f) ≤ bs(f) ≤ C(f)`.
 
 ## References
 
-* [S. Arora, B. Barak, *Computational Complexity: A Modern Approach*][AroraBarak2009],
+* [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]
diff --git a/references.bib b/references.bib
index 96917c56c..1c3cbeefe 100644
--- a/references.bib
+++ b/references.bib
@@ -53,16 +53,6 @@ @article{AngluinLaird1988
   doi          = {10.1007/BF00116829}
 }
 
-@book{AroraBarak2009,
-  author    = {Arora, Sanjeev and Barak, Boaz},
-  title     = {Computational Complexity: A Modern Approach},
-  year      = {2009},
-  isbn      = {9780521424264},
-  publisher = {Cambridge University Press},
-  address   = {New York},
-  url       = {https://theory.cs.princeton.edu/complexity/}
-}
-
 @book{Baader1998,
 author = {Baader, Franz and Nipkow, Tobias},
 title = {Term rewriting and all that},

From b5ed7df2d1350ff392f3ca050ff3539595f4932a Mon Sep 17 00:00:00 2001
From: Vignesh Karri <vigneshkarri5@gmail.com>
Date: Fri, 18 Sep 2026 23:47:45 +0530
Subject: [PATCH 3/7] doc(QueryComplexity): use Arora-Barak subscript notation
 for pointwise measures

---
 .../QueryComplexity/Measures.lean             | 28 +++++++++----------
 CslibTests/QueryComplexity.lean               |  2 +-
 2 files changed, 15 insertions(+), 15 deletions(-)

diff --git a/Cslib/Computability/QueryComplexity/Measures.lean b/Cslib/Computability/QueryComplexity/Measures.lean
index 2d55eecc9..89f25d9a6 100644
--- a/Cslib/Computability/QueryComplexity/Measures.lean
+++ b/Cslib/Computability/QueryComplexity/Measures.lean
@@ -65,19 +65,19 @@ lemma mem_sensitiveCoords {f : BoolFunc n} {x : Cube n} {i : Fin n} :
     i ∈ sensitiveCoords f x ↔ IsSensitiveCoord f x i := by
   simp [sensitiveCoords]
 
-/-- `s(f, x)` is the number of sensitive coordinates in input `x`. -/
+/-- `sₓ(f)` is the number of sensitive coordinates in input `x`. -/
 def pointSensitivity (f : BoolFunc n) (x : Cube n) : ℕ := (sensitiveCoords f x).card
 
 /-- `s(f)`. -/
 def sensitivity (f : BoolFunc n) : ℕ := Finset.univ.sup (pointSensitivity f)
 
-/-- Lower-bound rule for `s(f, x)`: exhibit a set of sensitive coordinates. -/
+/-- 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
 
-/-- `s(f, x) ≤ s(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)
@@ -114,19 +114,19 @@ lemma mem_sensitiveFamilies {f : BoolFunc n} {x : Cube n} {F : Finset (Block n)}
     F ∈ sensitiveFamilies f x ↔ IsSensitiveFamily f x F := by
   simp [sensitiveFamilies]
 
-/-- `bs(f, x)`. -/
+/-- `bsₓ(f)`. -/
 def pointBlockSensitivity (f : BoolFunc n) (x : Cube n) : ℕ :=
   (sensitiveFamilies f x).sup Finset.card
 
 /-- `bs(f)`. -/
 def blockSensitivity (f : BoolFunc n) : ℕ := Finset.univ.sup (pointBlockSensitivity f)
 
-/-- Lower-bound rule for `bs(f, x)`: exhibit one sensitive family. -/
+/-- 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)
 
-/-- `bs(f, x) ≤ bs(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)
@@ -156,7 +156,7 @@ 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, x)` of them. -/
+/-- 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 :=
@@ -175,7 +175,7 @@ lemma isSensitiveFamily_singletonFamily {f : BoolFunc n} {x : Cube n} :
     obtain ⟨j, -, rfl⟩ := mem_singletonFamily.mp hQ
     exact Finset.disjoint_singleton.mpr fun h => hPQ (by rw [h])
 
-/-- Pointwise: `s(f, x) ≤ bs(f, x)`. -/
+/-- 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
@@ -241,15 +241,15 @@ lemma ofCube_mem_certificates (f : BoolFunc n) (x : Cube n) : ofCube x ∈ certi
   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, x)` is a minimum over a non-empty set. -/
+/-- 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⟩
 
-/-- `C(f, x)`: the size of the smallest certificate. -/
+/-- `Cₓ(f)`: the size of the smallest certificate. -/
 def pointCertificateComplexity (f : BoolFunc n) (x : Cube n) : ℕ :=
   (certificates f x).inf' (certificates_nonempty f x) size
 
-/-- Upper-bound rule for `C(f, x)`: exhibit one certificate. -/
+/-- Upper-bound rule for `Cₓ(f)`: exhibit one certificate. -/
 lemma pointCertificateComplexity_le {f : BoolFunc n} {x : Cube n} {C : Assignment n}
     (h : C ∈ certificates f x) : pointCertificateComplexity f x ≤ size C :=
   Finset.inf'_le _ h
@@ -258,12 +258,12 @@ lemma pointCertificateComplexity_le {f : BoolFunc n} {x : Cube n} {C : Assignmen
 def certificateComplexity (f : BoolFunc n) : ℕ :=
   Finset.univ.sup (pointCertificateComplexity f)
 
-/-- `C(f, x) ≤ C(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, x) ≤ n`: reading off the whole input is a certificate. -/
+/-- `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)
@@ -296,7 +296,7 @@ lemma card_le_size_of_isSensitiveFamily {f : BoolFunc n} {x : Cube n}
       (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, x) ≤ C(f, x)`. -/
+/-- Pointwise: `bsₓ(f) ≤ Cₓ(f)`. -/
 theorem pointBlockSensitivity_le_pointCertificateComplexity
     (f : BoolFunc n) (x : Cube n) :
     pointBlockSensitivity f x ≤ pointCertificateComplexity f x :=
diff --git a/CslibTests/QueryComplexity.lean b/CslibTests/QueryComplexity.lean
index 605b761c5..5d97a2ed8 100644
--- a/CslibTests/QueryComplexity.lean
+++ b/CslibTests/QueryComplexity.lean
@@ -103,7 +103,7 @@ 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, x) = 2` everywhere. -/
+/-- Two agreeing bits are a certificate, so `Cₓ(f) = 2` everywhere. -/
 example : pointCertificateComplexity maj3 ![true, true, false] = 2 := by decide
 
 /-! ## Constant functions

From 9cdc16417ee08a35a84fd156c50653a8d7991a94 Mon Sep 17 00:00:00 2001
From: Vignesh Karri <vigneshkarri5@gmail.com>
Date: Sat, 19 Sep 2026 00:44:49 +0530
Subject: [PATCH 4/7] explain definitions and fix notation.

---
 Cslib/Computability/QueryComplexity/Defs.lean | 13 ++-------
 .../QueryComplexity/Measures.lean             | 27 ++++++++++---------
 2 files changed, 17 insertions(+), 23 deletions(-)

diff --git a/Cslib/Computability/QueryComplexity/Defs.lean b/Cslib/Computability/QueryComplexity/Defs.lean
index 13a2fa93b..dbae633a3 100644
--- a/Cslib/Computability/QueryComplexity/Defs.lean
+++ b/Cslib/Computability/QueryComplexity/Defs.lean
@@ -42,7 +42,8 @@ variable {n : ℕ}
 /-- Bit string of length `n`. -/
 abbrev Cube (n : ℕ) : Type := Fin n → Bool
 
-/-- `f : {0,1}ⁿ → {0,1}`. -/
+/-- A Boolean function on `n` inputs: a map from bit strings of length `n` to a single bit,
+`f : {0,1}ⁿ → {0,1}`. -/
 abbrev BoolFunc (n : ℕ) : Type := Cube n → Bool
 
 /-- A block: a set of coordinates. -/
@@ -53,16 +54,6 @@ 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)
 
-/-- The flipped coordinate reads back negated. -/
-@[simp]
-lemma flipBit_self (x : Cube n) (i : Fin n) : flipBit x i i = !x i :=
-  Function.update_self ..
-
-/-- Every other coordinate is left alone. -/
-@[simp]
-lemma flipBit_of_ne {x : Cube n} {i j : Fin n} (h : j ≠ i) : flipBit x i j = x j :=
-  Function.update_of_ne h ..
-
 /-- `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
diff --git a/Cslib/Computability/QueryComplexity/Measures.lean b/Cslib/Computability/QueryComplexity/Measures.lean
index 89f25d9a6..fbaef25ea 100644
--- a/Cslib/Computability/QueryComplexity/Measures.lean
+++ b/Cslib/Computability/QueryComplexity/Measures.lean
@@ -17,7 +17,7 @@ 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)`.
+the chain `s(f) ≤ bs(f) ≤ C(f)`. Notation follows [AroraBarak09].
 
 ## Main definitions
 
@@ -65,10 +65,10 @@ lemma mem_sensitiveCoords {f : BoolFunc n} {x : Cube n} {i : Fin n} :
     i ∈ sensitiveCoords f x ↔ IsSensitiveCoord f x i := by
   simp [sensitiveCoords]
 
-/-- `sₓ(f)` is the number of sensitive coordinates in input `x`. -/
+/-- The number of sensitive coordinates in input `x`, usually denoted `sₓ(f)`. -/
 def pointSensitivity (f : BoolFunc n) (x : Cube n) : ℕ := (sensitiveCoords f x).card
 
-/-- `s(f)`. -/
+/-- 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. -/
@@ -77,7 +77,7 @@ lemma card_le_pointSensitivity {f : BoolFunc n} {x : Cube n} {S : Finset (Fin n)
   apply Finset.card_le_card
   simpa [Finset.subset_iff] using h
 
-/-- `sₓ(f) ≤ s(f)`. -/
+/-- 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)
@@ -114,11 +114,13 @@ lemma mem_sensitiveFamilies {f : BoolFunc n} {x : Cube n} {F : Finset (Block n)}
     F ∈ sensitiveFamilies f x ↔ IsSensitiveFamily f x F := by
   simp [sensitiveFamilies]
 
-/-- `bsₓ(f)`. -/
+/-- 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
 
-/-- `bs(f)`. -/
+/-- 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. -/
@@ -126,7 +128,7 @@ lemma card_le_pointBlockSensitivity {f : BoolFunc n} {x : Cube n} {F : Finset (B
     (h : IsSensitiveFamily f x F) : F.card ≤ pointBlockSensitivity f x :=
   Finset.le_sup (mem_sensitiveFamilies.mpr h)
 
-/-- `bsₓ(f) ≤ bs(f)`. -/
+/-- 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)
@@ -180,7 +182,7 @@ theorem pointSensitivity_le_pointBlockSensitivity (f : BoolFunc n) (x : Cube n)
     pointSensitivity f x ≤ pointBlockSensitivity f x :=
   card_singletonFamily ▸ card_le_pointBlockSensitivity isSensitiveFamily_singletonFamily
 
-/-- `s(f) ≤ bs(f)`. -/
+/-- 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
@@ -245,7 +247,7 @@ lemma ofCube_mem_certificates (f : BoolFunc n) (x : Cube n) : ofCube x ∈ certi
 lemma certificates_nonempty (f : BoolFunc n) (x : Cube n) : (certificates f x).Nonempty :=
   ⟨ofCube x, ofCube_mem_certificates f x⟩
 
-/-- `Cₓ(f)`: the size of the smallest certificate. -/
+/-- 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
 
@@ -254,11 +256,11 @@ lemma pointCertificateComplexity_le {f : BoolFunc n} {x : Cube n} {C : Assignmen
     (h : C ∈ certificates f x) : pointCertificateComplexity f x ≤ size C :=
   Finset.inf'_le _ h
 
-/-- `C(f)`. -/
+/-- The maximum over all inputs of the smallest certificate size, denoted `C(f)`. -/
 def certificateComplexity (f : BoolFunc n) : ℕ :=
   Finset.univ.sup (pointCertificateComplexity f)
 
-/-- `Cₓ(f) ≤ C(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)
@@ -303,7 +305,8 @@ theorem pointBlockSensitivity_le_pointCertificateComplexity
   Finset.sup_le fun _ hF => Finset.le_inf' _ _ fun _ hC =>
     card_le_size_of_isSensitiveFamily (mem_sensitiveFamilies.mp hF) hC
 
-/-- `bs(f) ≤ C(f)`. -/
+/-- 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 _ =>

From 87b847b44e8691bbd5573a91314b01b639bd1816 Mon Sep 17 00:00:00 2001
From: Vignesh Karri <vigneshkarri5@gmail.com>
Date: Fri, 18 Sep 2026 22:04:15 +0530
Subject: [PATCH 5/7] feat(QueryComplexity): decision tree complexity

---
 .../QueryComplexity/DecisionTree.lean         | 338 ++++++++++++++++++
 1 file changed, 338 insertions(+)
 create mode 100644 Cslib/Computability/QueryComplexity/DecisionTree.lean

diff --git a/Cslib/Computability/QueryComplexity/DecisionTree.lean b/Cslib/Computability/QueryComplexity/DecisionTree.lean
new file mode 100644
index 000000000..9ea649a70
--- /dev/null
+++ b/Cslib/Computability/QueryComplexity/DecisionTree.lean
@@ -0,0 +1,338 @@
+/-
+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*][AroraBarak2009],
+  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`. Nothing forbids querying the same
+coordinate twice on a route. -/
+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
+
+/-- A leaf asks nothing. -/
+@[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. Always at most
+`depth`, with equality when `x` takes a longest path. -/
+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
+
+/-- A leaf asks nothing, whatever the input. -/
+@[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. The recursion is on the list rather than on `n`, which
+keeps every subtree over the same coordinate type. -/
+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 generalised form the induction needs. -/
+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 =>
+    -- Nothing left to query, so `h` says `acc` and `x` agree at *every* coordinate.
+    have hacc : acc = x := by grind
+    simp [bruteForce, eval, hacc]
+  | cons i is ih =>
+    -- Whichever branch `x` takes, the accumulator now records `x i` correctly, so the
+    -- invariant survives and the induction hypothesis applies to that subtree.
+    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
+      · -- the coordinate just answered: the update wrote exactly `x i`
+        subst hji; simp [hb]
+      · -- any other coordinate is untouched, so the old agreement carries over
+        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)`: exhibit a single tree computing `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 — `fullTree` lives in it. Everything
+below needs this; without it `complexity f` could be `sInf ∅ = 0` for all we know. -/
+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. A non-empty set of naturals attains its infimum
+(`Nat.sInf_mem`), so the minimum in `complexity` is realised by an actual tree.
+Every argument that begins "take an optimal decision tree for `f`" needs this. -/
+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)
+
+/-- Lower-bound rule for `D(f)`: to bound `D(f)` from below, bound the depth of
+every tree computing `f`. The counterpart of `complexity_le_depth`. -/
+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)
+
+/-- Everything a path records about `x` is `x`'s own value. Needed before `routing`,
+because a coordinate may be queried twice on one route. -/
+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])
+
+/-- The routing lemma. If `y` answers every query the tree asked of `x` the same
+way, the tree cannot tell them apart. This is the formal content of "the adversary
+answers consistently", and the engine of `C(f) ≤ D(f)`. -/
+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)
+
+/-- A path fixes no more coordinates than the tree made queries. The inequality can
+be strict: a re-queried coordinate is charged twice but occupies one slot. -/
+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. Anything agreeing with the route `x` took reaches
+the same leaf (`routing`), so `f` is pinned to `f x` on the whole subcube. -/
+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, x) ≤ D(f)`, by running the chain
+`C(f, x) ≤ 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

From 71d56dde5539c941d4b94fee9343cc7de0dc7444 Mon Sep 17 00:00:00 2001
From: Vignesh Karri <vigneshkarri5@gmail.com>
Date: Fri, 18 Sep 2026 23:49:55 +0530
Subject: [PATCH 6/7] doc(QueryComplexity): tighten DecisionTree docstrings,
 AroraBarak09 key, subscript notation

---
 .../QueryComplexity/DecisionTree.lean         | 56 +++++++------------
 1 file changed, 19 insertions(+), 37 deletions(-)

diff --git a/Cslib/Computability/QueryComplexity/DecisionTree.lean b/Cslib/Computability/QueryComplexity/DecisionTree.lean
index 9ea649a70..aedf22a1d 100644
--- a/Cslib/Computability/QueryComplexity/DecisionTree.lean
+++ b/Cslib/Computability/QueryComplexity/DecisionTree.lean
@@ -38,7 +38,7 @@ that input. Together with `Measures.lean` that gives the chain
 
 ## References
 
-* [S. Arora, B. Barak, *Computational Complexity: A Modern Approach*][AroraBarak2009],
+* [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:
@@ -55,8 +55,7 @@ variable {n : ℕ}
 
 /-- 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`. Nothing forbids querying the same
-coordinate twice on a route. -/
+`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
@@ -85,7 +84,6 @@ def depth : DecisionTree n → ℕ
   | .leaf _ => 0
   | .node _ l r => max l.depth r.depth + 1
 
-/-- A leaf asks nothing. -/
 @[simp]
 lemma depth_leaf (b : Bool) : (leaf b : DecisionTree n).depth = 0 := rfl
 
@@ -102,13 +100,11 @@ 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. Always at most
-`depth`, with equality when `x` takes a longest path. -/
+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
 
-/-- A leaf asks nothing, whatever the input. -/
 @[simp]
 lemma cost_leaf (b : Bool) (x : Cube n) : (leaf b : DecisionTree n).cost x = 0 := rfl
 
@@ -136,8 +132,7 @@ then reads off the answer. This proves the set in the `complexity` definition is
 
 /-- 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. The recursion is on the list rather than on `n`, which
-keeps every subtree over the same coordinate type. -/
+value `acc` came in with. -/
 def bruteForce (f : BoolFunc n) : List (Fin n) → Cube n → DecisionTree n
   | [], acc => .leaf (f acc)
   | i :: is, acc =>
@@ -152,26 +147,21 @@ theorem depth_bruteForce (is : List (Fin n)) (acc : Cube n) (f : BoolFunc n) :
   | cons head tail tail_ih =>
     simp [bruteForce, tail_ih]
 
-/-- Correctness, in the generalised form the induction needs. -/
+/-- 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 =>
-    -- Nothing left to query, so `h` says `acc` and `x` agree at *every* coordinate.
     have hacc : acc = x := by grind
     simp [bruteForce, eval, hacc]
   | cons i is ih =>
-    -- Whichever branch `x` takes, the accumulator now records `x i` correctly, so the
-    -- invariant survives and the induction hypothesis applies to that subtree.
     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
-      · -- the coordinate just answered: the update wrote exactly `x i`
-        subst hji; simp [hb]
-      · -- any other coordinate is untouched, so the old agreement carries over
-        rw [Function.update_of_ne hji]
+      · 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
@@ -199,14 +189,13 @@ theorem depth_fullTree (f : BoolFunc n) : (fullTree f).depth = n := by
 noncomputable def complexity (f : BoolFunc n) : ℕ :=
   sInf {k | ∃ t : DecisionTree n, t.Computes f ∧ t.depth = k}
 
-/-- Upper-bound rule for `D(f)`: exhibit a single tree computing `f`. -/
+/-- 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 — `fullTree` lives in it. Everything
-below needs this; without it `complexity f` could be `sInf ∅ = 0` for all we know. -/
+/-- 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⟩
@@ -215,30 +204,25 @@ theorem depths_nonempty (f : BoolFunc n) :
 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. A non-empty set of naturals attains its infimum
-(`Nat.sInf_mem`), so the minimum in `complexity` is realised by an actual tree.
-Every argument that begins "take an optimal decision tree for `f`" needs this. -/
+/-- 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)
 
-/-- Lower-bound rule for `D(f)`: to bound `D(f)` from below, bound the depth of
-every tree computing `f`. The counterpart of `complexity_le_depth`. -/
 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
+/-- 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)
 
-/-- Everything a path records about `x` is `x`'s own value. Needed before `routing`,
-because a coordinate may be queried twice on one route. -/
+/-- 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]
@@ -259,9 +243,8 @@ lemma agrees_of_agrees_update {C : Assignment n} {x y : Cube n} {j : Fin n}
     rw [hy, hC k c hk]
   · exact h k c (by rwa [Function.update_of_ne hkj])
 
-/-- The routing lemma. If `y` answers every query the tree asked of `x` the same
-way, the tree cannot tell them apart. This is the formal content of "the adversary
-answers consistently", and the engine of `C(f) ≤ D(f)`. -/
+/-- 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
@@ -290,8 +273,8 @@ lemma support_update_subset (C : Assignment n) (j : Fin n) (b : Bool) :
   · rw [mem_support, Function.update_of_ne hij] at hi
     exact Finset.mem_insert_of_mem (mem_support.mpr hi)
 
-/-- A path fixes no more coordinates than the tree made queries. The inequality can
-be strict: a re-queried coordinate is charged twice but occupies one slot. -/
+/-- 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]
@@ -311,14 +294,13 @@ theorem size_path_le_cost (t : DecisionTree n) (x : Cube n) : size (path t x) 
         _ ≤ (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. Anything agreeing with the route `x` took reaches
-the same leaf (`routing`), so `f` is pinned to `f x` on the whole subcube. -/
+/-- 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, x) ≤ D(f)`, by running the chain
-`C(f, x) ≤ size (path t x) ≤ cost t x ≤ depth t` over every tree computing `f`. -/
+/-- 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

From 7fd39ab2728d531e03bda7015d58c67fae76f19a Mon Sep 17 00:00:00 2001
From: Vignesh Karri <vigneshkarri5@gmail.com>
Date: Sat, 19 Sep 2026 01:04:32 +0530
Subject: [PATCH 7/7] chore(QueryComplexity): register DecisionTree in
 Cslib.lean

---
 Cslib.lean | 1 +
 1 file changed, 1 insertion(+)

diff --git a/Cslib.lean b/Cslib.lean
index 34b090c71..beaff4b59 100644
--- a/Cslib.lean
+++ b/Cslib.lean
@@ -64,6 +64,7 @@ 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