diff --git a/Cslib.lean b/Cslib.lean
index 2b04deb7fc..054dd1414a 100644
--- a/Cslib.lean
+++ b/Cslib.lean
@@ -2,6 +2,18 @@ module  -- shake: keep-all --deprecated_module: ignore
 
 public import Cslib.Algorithms.CCS.VendingMachine
 public import Cslib.Algorithms.Lean.MergeSort.MergeSort
+public import Cslib.Algorithms.Lean.Query.Arith.Defs
+public import Cslib.Algorithms.Lean.Query.Arith.Lemmas
+public import Cslib.Algorithms.Lean.Query.Bounds
+public import Cslib.Algorithms.Lean.Query.FreeM
+public import Cslib.Algorithms.Lean.Query.Sort.Insertion.Defs
+public import Cslib.Algorithms.Lean.Query.Sort.Insertion.Lemmas
+public import Cslib.Algorithms.Lean.Query.Sort.IsSort
+public import Cslib.Algorithms.Lean.Query.Sort.LEQuery
+public import Cslib.Algorithms.Lean.Query.Sort.LowerBound
+public import Cslib.Algorithms.Lean.Query.Sort.Merge.Bounds
+public import Cslib.Algorithms.Lean.Query.Sort.Merge.Defs
+public import Cslib.Algorithms.Lean.Query.Sort.Merge.Lemmas
 public import Cslib.Algorithms.Lean.Sort.Insertion
 public import Cslib.Algorithms.Lean.Sort.Merge
 public import Cslib.Algorithms.Lean.TimeM
diff --git a/Cslib/Algorithms/Lean/Query/Arith/Defs.lean b/Cslib/Algorithms/Lean/Query/Arith/Defs.lean
new file mode 100644
index 0000000000..0d9abad592
--- /dev/null
+++ b/Cslib/Algorithms/Lean/Query/Arith/Defs.lean
@@ -0,0 +1,78 @@
+/-
+Copyright (c) 2026 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Kim Morrison
+-/
+module
+
+public import Cslib.Algorithms.Lean.Query.FreeM
+
+/-! # Arithmetic Queries and Complex Multiplication
+
+A simple example showing how to use `FreeM.cost` with variable/parametrized query costs.
+
+`ArithQuery α` supports addition, subtraction, and multiplication, each with
+independently parametrized costs. Complex number multiplication provides a toy example
+where two algorithms (naive and Gauss's trick) trade multiplications for additions,
+and the optimal choice depends on the cost ratio.
+-/
+
+public section
+
+namespace Cslib.Query
+
+/-- Arithmetic queries: addition, subtraction, and multiplication. -/
+inductive ArithQuery (α : Type) : Type → Type where
+  | add (a b : α) : ArithQuery α α
+  | sub (a b : α) : ArithQuery α α
+  | mul (a b : α) : ArithQuery α α
+
+namespace ArithQuery
+
+/-- Lift `ArithQuery.add a b` into a `FreeM` that returns the sum. -/
+abbrev doAdd (a b : α) : FreeM (ArithQuery α) α := FreeM.lift (.add a b)
+/-- Lift `ArithQuery.sub a b` into a `FreeM` that returns the difference. -/
+abbrev doSub (a b : α) : FreeM (ArithQuery α) α := FreeM.lift (.sub a b)
+/-- Lift `ArithQuery.mul a b` into a `FreeM` that returns the product. -/
+abbrev doMul (a b : α) : FreeM (ArithQuery α) α := FreeM.lift (.mul a b)
+
+/-- An honest oracle interprets arithmetic queries using the actual ring operations. -/
+@[expose] def honest [Add α] [Sub α] [Mul α] {ι : Type} : ArithQuery α ι → ι
+  | .add a b => a + b
+  | .sub a b => a - b
+  | .mul a b => a * b
+
+/-- Weighted cost model for arithmetic queries. Subtraction costs the same as addition
+    (both are linear-time on bignums). -/
+@[expose] def weight (c_add c_mul : Nat) {ι : Type} : ArithQuery α ι → Nat
+  | .add _ _ => c_add
+  | .sub _ _ => c_add
+  | .mul _ _ => c_mul
+
+end ArithQuery
+
+/-- Naive complex multiplication: `(a + bi)(c + di) = (ac - bd) + (ad + bc)i`.
+    Uses 4 multiplications, 1 subtraction, 1 addition. -/
+@[expose] def complexMulNaive (a b c d : α) : FreeM (ArithQuery α) (α × α) := do
+  let ac ← ArithQuery.doMul a c
+  let bd ← ArithQuery.doMul b d
+  let ad ← ArithQuery.doMul a d
+  let bc ← ArithQuery.doMul b c
+  let real ← ArithQuery.doSub ac bd
+  let imag ← ArithQuery.doAdd ad bc
+  return (real, imag)
+
+/-- Gauss's trick for complex multiplication: computes `(a+b)(c+d)` to save one
+    multiplication, at the cost of extra additions and subtractions.
+    Uses 3 multiplications, 2 subtractions, 3 additions. -/
+@[expose] def complexMulGauss (a b c d : α) : FreeM (ArithQuery α) (α × α) := do
+  let ac ← ArithQuery.doMul a c
+  let bd ← ArithQuery.doMul b d
+  let apb ← ArithQuery.doAdd a b
+  let cpd ← ArithQuery.doAdd c d
+  let abcd ← ArithQuery.doMul apb cpd
+  let real ← ArithQuery.doSub ac bd
+  let imag ← ArithQuery.doSub abcd (← ArithQuery.doAdd ac bd)
+  return (real, imag)
+
+end Cslib.Query
diff --git a/Cslib/Algorithms/Lean/Query/Arith/Lemmas.lean b/Cslib/Algorithms/Lean/Query/Arith/Lemmas.lean
new file mode 100644
index 0000000000..97e43e6afc
--- /dev/null
+++ b/Cslib/Algorithms/Lean/Query/Arith/Lemmas.lean
@@ -0,0 +1,75 @@
+/-
+Copyright (c) 2026 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Kim Morrison
+-/
+module
+
+public import Cslib.Algorithms.Lean.Query.Arith.Defs
+import Mathlib.Tactic.Ring
+public import Mathlib.Algebra.Ring.Defs
+
+/-! # Complex Multiplication: Correctness and Cost Analysis
+
+A simple example showing how to use `FreeM.cost` with variable/parametrized query costs.
+
+We prove that both `complexMulNaive` and `complexMulGauss` correctly compute
+complex multiplication when given an honest oracle, and compute their exact
+costs under a parametric weight function. The cost theorems hold for *any* oracle
+(not just honest ones), because both algorithms are straight-line (no branching
+on query results).
+-/
+
+open Cslib.Query
+
+public section
+
+namespace Cslib.Query
+
+variable {α : Type}
+
+/-! ## Correctness -/
+
+theorem complexMulNaive_eval_honest [Add α] [Sub α] [Mul α] (a b c d : α) :
+    (complexMulNaive a b c d).eval ArithQuery.honest = (a * c - b * d, a * d + b * c) := by
+  simp [complexMulNaive, ArithQuery.doMul, ArithQuery.doSub, ArithQuery.doAdd, ArithQuery.honest]
+
+theorem complexMulGauss_eval_honest [CommRing α] (a b c d : α) :
+    (complexMulGauss a b c d).eval ArithQuery.honest = (a * c - b * d, a * d + b * c) := by
+  simp [complexMulGauss, ArithQuery.doMul, ArithQuery.doSub, ArithQuery.doAdd, ArithQuery.honest]
+  ring
+
+/-! ## Exact cost counts -/
+
+theorem complexMulNaive_cost (oracle : {ι : Type} → ArithQuery α ι → ι)
+    (c_add c_mul : Nat) (a b c d : α) :
+    (complexMulNaive a b c d).cost oracle (ArithQuery.weight c_add c_mul) =
+      4 * c_mul + 2 * c_add := by
+  simp [complexMulNaive, ArithQuery.doMul, ArithQuery.doSub, ArithQuery.doAdd, ArithQuery.weight]
+  omega
+
+theorem complexMulGauss_cost (oracle : {ι : Type} → ArithQuery α ι → ι)
+    (c_add c_mul : Nat) (a b c d : α) :
+    (complexMulGauss a b c d).cost oracle (ArithQuery.weight c_add c_mul) =
+      3 * c_mul + 5 * c_add := by
+  simp [complexMulGauss, ArithQuery.doMul, ArithQuery.doSub, ArithQuery.doAdd, ArithQuery.weight]
+  omega
+
+/-! ## Crossover: Gauss beats naive when multiplication costs at least 3× addition -/
+
+theorem gauss_le_naive (oracle : {ι : Type} → ArithQuery α ι → ι)
+    (c_add c_mul : Nat) (a b c d : α) (h : 3 * c_add ≤ c_mul) :
+    (complexMulGauss a b c d).cost oracle (ArithQuery.weight c_add c_mul) ≤
+      (complexMulNaive a b c d).cost oracle (ArithQuery.weight c_add c_mul) := by
+  rw [complexMulGauss_cost, complexMulNaive_cost]
+  omega
+
+theorem gauss_le_naive_iff (oracle : {ι : Type} → ArithQuery α ι → ι)
+    (c_add c_mul : Nat) (a b c d : α) :
+    (complexMulGauss a b c d).cost oracle (ArithQuery.weight c_add c_mul) ≤
+      (complexMulNaive a b c d).cost oracle (ArithQuery.weight c_add c_mul) ↔
+        3 * c_add ≤ c_mul := by
+  rw [complexMulGauss_cost, complexMulNaive_cost]
+  omega
+
+end Cslib.Query
diff --git a/Cslib/Algorithms/Lean/Query/Bounds.lean b/Cslib/Algorithms/Lean/Query/Bounds.lean
new file mode 100644
index 0000000000..19077942d2
--- /dev/null
+++ b/Cslib/Algorithms/Lean/Query/Bounds.lean
@@ -0,0 +1,54 @@
+/-
+Copyright (c) 2026 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Sebastian Graf, Kim Morrison, Shreyas Srinivas
+-/
+module
+
+public import Cslib.Algorithms.Lean.Query.FreeM
+public import Mathlib.Order.Monotone.Defs
+
+/-! # Upper and Lower Bounds for Query Complexity
+
+Definitions of upper and lower bounds on the number of queries a program makes,
+quantified over oracles.
+-/
+
+public section
+
+namespace Cslib.Query
+
+universe u v w
+
+variable {α : Type w} {Q : Type u → Type v} {β : Type u}
+
+/-- Upper bound: for all oracles, inputs of size ≤ n make at most `bound n` queries. -/
+@[expose] def UpperBound (prog : α → FreeM Q β)
+    (size : α → Nat) (bound : Nat → Nat) : Prop :=
+  ∀ (oracle : {ι : Type u} → Q ι → ι) (n : Nat) (x : α),
+    size x ≤ n → (prog x).countQueries oracle ≤ bound n
+
+/-- Lower bound: for every size n, there exists an input of size at most n and an oracle
+    making the program perform ≥ `bound n` queries. -/
+@[expose] def LowerBound (prog : α → FreeM Q β)
+    (size : α → Nat) (bound : Nat → Nat) : Prop :=
+  ∀ (n : Nat), ∃ (x : α), size x ≤ n ∧
+    ∃ (oracle : {ι : Type u} → Q ι → ι), bound n ≤ (prog x).countQueries oracle
+
+/-- To prove an `UpperBound` with a monotone bound function, it suffices to bound the
+    query count of each input by `bound` at its own size. -/
+theorem UpperBound.of_pointwise {prog : α → FreeM Q β} {size : α → Nat} {bound : Nat → Nat}
+    (hmono : Monotone bound)
+    (h : ∀ (oracle : {ι : Type u} → Q ι → ι) (x : α),
+      (prog x).countQueries oracle ≤ bound (size x)) :
+    UpperBound prog size bound :=
+  fun oracle _n x hx => (h oracle x).trans (hmono hx)
+
+/-- A lower bound for a program never exceeds an upper bound for the same program and
+    size function. -/
+theorem LowerBound.le_upperBound {prog : α → FreeM Q β} {size : α → Nat} {l u : Nat → Nat}
+    (hl : LowerBound prog size l) (hu : UpperBound prog size u) (n : Nat) : l n ≤ u n := by
+  obtain ⟨x, hx, oracle, hbound⟩ := hl n
+  exact hbound.trans (hu oracle n x hx)
+
+end Cslib.Query
diff --git a/Cslib/Algorithms/Lean/Query/FreeM.lean b/Cslib/Algorithms/Lean/Query/FreeM.lean
new file mode 100644
index 0000000000..4d4afc7857
--- /dev/null
+++ b/Cslib/Algorithms/Lean/Query/FreeM.lean
@@ -0,0 +1,305 @@
+/-
+Copyright (c) 2026 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Sebastian Graf, Kim Morrison, Shreyas Srinivas
+-/
+module
+
+public import Cslib.Foundations.Control.Monad.Free
+public import Cslib.Algorithms.Lean.TimeM
+public import Mathlib.Combinatorics.Pigeonhole
+public import Mathlib.Data.Fintype.Card
+public import Mathlib.Data.Nat.Log
+public import Mathlib.Data.Set.Function
+public import Mathlib.SetTheory.Cardinal.Finite
+
+/-! # FreeM: query/cost interpreters and lower-bound lemma
+
+This file adds query-complexity interpreters to `FreeM F α`, where the type constructor
+`F : Type u → Type v` represents a query type mapping each query to its response type.
+
+The key operations are:
+- `FreeM.eval oracle p`: evaluate `p` by answering each query using `oracle`
+- `FreeM.countQueries oracle p`: count queries along the oracle-determined path
+- `FreeM.cost oracle weight p`: weighted query cost in any additive monoid
+
+The program `p` must be fixed independently of `oracle`. Arbitrary pure computation embedded
+in `p` is uncharged, so `countQueries` and `cost` measure query complexity rather than total
+runtime. However, pure code cannot inspect oracle responses: those enter only through
+`FreeM.lift`.
+
+This provides an alternative to the `TimeM`-based cost analysis in
+`Cslib.Algorithms.Lean.MergeSort.MergeSort`: here query counting is structural (derived from
+the `FreeM` tree) rather than annotation-based.
+
+The combinatorial lower-bound lemma `FreeM.exists_countQueries_ge_clog` says: if `n` distinct
+oracles produce `n` distinct evaluation results from a program whose every response type has
+cardinality at most `r`, then some oracle makes at least `⌈log_r n⌉` queries. The proof uses
+the adversarial/partition argument: at each query node, the oracles split by their answer,
+and the largest fiber still produces distinct results in the corresponding subtree.
+
+## Setting up your own query type
+
+1. Define an inductive `Q : Type u → Type v` whose constructors are the queries, indexed by
+   their response types (see `LEQuery`, `ArithQuery`).
+2. Wrap each constructor with `FreeM.lift` to obtain one-step programs (`LEQuery.ask`).
+3. Write algorithms in `do`-notation as values of `FreeM Q α`.
+4. Prove correctness by relating `FreeM.eval` to a reference implementation, and bounds by
+   equational reasoning with the `countQueries`/`cost` simp lemmas; state them with
+   `Cslib.Query.UpperBound`/`Cslib.Query.LowerBound`.
+-/
+
+public section
+
+open Cslib.Algorithms.Lean (TimeM)
+open scoped Cardinal
+
+namespace Cslib.FreeM
+
+universe u v t w
+
+variable {F : Type u → Type v} {α β : Type u}
+
+/-- `TimeM.ret` distributes across `FreeM.liftM`. -/
+@[simp]
+theorem timeMRet_liftM {T : Type t} [AddMonoid T] (interp : {ι : Type u} → F ι → TimeM T ι)
+    (p : FreeM F α) :
+    (p.liftM interp).ret = Id.run (p.liftM fun i => pure (interp i).ret) :=
+  Algorithms.Lean.TimeM.isMonadHom_pure_ret.map_freeMLiftM _ _
+
+/-! ## Interpreters
+
+All three interpreters (`eval`, `cost`, `countQueries`) are defined as `liftM` interpretations
+into target monads, routing them through the universal property of the free monad rather
+than direct pattern-match on `FreeM`'s constructors:
+
+- `eval` interprets into `Id`.
+- `cost` interprets into a `TimeM` accumulator monad (a value paired with a running cost in
+  an arbitrary additive monoid).
+- `countQueries` is `cost` with unit weight.
+
+The pure and lift-then-bind simp lemmas (`eval_pure`, `eval_liftBind`, `cost_pure`,
+`cost_liftBind`, `countQueries_pure`, `countQueries_liftBind`) all reduce by `rfl`, giving the
+same proof ergonomics as direct pattern-match definitions while honouring the universal
+property as the primary abstraction. -/
+
+/-- Evaluate a program by answering each query using `oracle`.
+Defined as `liftM` to `Id`, the canonical interpreter into pure values. -/
+@[expose] def eval (oracle : {ι : Type u} → F ι → ι) (p : FreeM F α) : α :=
+  Id.run <| p.liftM fun i => pure (oracle i)
+
+/-- Weighted query cost in an additive monoid: each query has a cost given by `weight`,
+accumulated along the oracle-determined path. Defined as `liftM` into `TimeM`. -/
+@[expose] def cost {T : Type t} [AddMonoid T] (oracle : {ι : Type u} → F ι → ι)
+    (weight : {ι : Type u} → F ι → T) (p : FreeM F α) : T :=
+  TimeM.time <| p.liftM fun op => ⟨oracle op, weight op⟩
+
+/-- Count the number of queries along the path determined by `oracle`.
+
+This is deliberately a `def` with its own simp lemmas, rather than an abbreviation for
+`cost oracle (fun _ => 1)`, so that goals display `countQueries`. -/
+@[expose] def countQueries (oracle : {ι : Type u} → F ι → ι) (p : FreeM F α) : Nat :=
+  cost oracle (fun _ => 1) p
+
+/-! ### Simp lemmas for `eval` -/
+
+@[simp] theorem eval_pure (oracle : {ι : Type u} → F ι → ι) (a : α) :
+    eval oracle (pure a : FreeM F α) = a := rfl
+
+@[simp] theorem eval_liftBind (oracle : {ι : Type u} → F ι → ι)
+    {ι : Type u} (op : F ι) (cont : ι → FreeM F α) :
+    eval oracle (FreeM.lift op >>= cont) = eval oracle (cont (oracle op)) := rfl
+
+@[simp] theorem eval_lift (oracle : {ι : Type u} → F ι → ι) {ι : Type u} (op : F ι) :
+    eval oracle (FreeM.lift op) = oracle op := rfl
+
+@[simp] theorem eval_bind (oracle : {ι : Type u} → F ι → ι)
+    (t : FreeM F α) (f : α → FreeM F β) :
+    eval oracle (t >>= f) = eval oracle (f (eval oracle t)) := by
+  simp [eval]
+
+@[simp] theorem eval_map (oracle : {ι : Type u} → F ι → ι)
+    (t : FreeM F α) (f : α → β) :
+    eval oracle (f <$> t) = f (eval oracle t) := by
+  simp [eval]
+
+theorem isMonadHom_pure_eval (oracle : {ι : Type u} → F ι → ι) :
+    IsMonadHom (FreeM F) Id (fun x => pure (x.eval oracle)) :=
+  .mk' (eval_pure oracle) (eval_bind oracle)
+
+/-! ### Simp lemmas for `cost` -/
+
+@[simp] theorem cost_pure {T : Type t} [AddMonoid T] (oracle : {ι : Type u} → F ι → ι)
+    (weight : {ι : Type u} → F ι → T) (a : α) :
+    cost oracle weight (pure a : FreeM F α) = 0 := rfl
+
+@[simp] theorem cost_liftBind {T : Type t} [AddMonoid T]
+    (oracle : {ι : Type u} → F ι → ι) (weight : {ι : Type u} → F ι → T)
+    {ι : Type u} (op : F ι) (cont : ι → FreeM F α) :
+    cost oracle weight (FreeM.lift op >>= cont) =
+      weight op + cost oracle weight (cont (oracle op)) := rfl
+
+@[simp] theorem cost_lift {T : Type t} [AddMonoid T]
+    (oracle : {ι : Type u} → F ι → ι) (weight : {ι : Type u} → F ι → T)
+    {ι : Type u} (op : F ι) :
+    cost oracle weight (FreeM.lift op) = weight op := by
+  simp [cost]
+
+@[simp] theorem cost_bind {T : Type t} [AddMonoid T] (oracle : {ι : Type u} → F ι → ι)
+    (weight : {ι : Type u} → F ι → T) (t : FreeM F α) (f : α → FreeM F β) :
+    cost oracle weight (t >>= f) =
+      cost oracle weight t + cost oracle weight (f (eval oracle t)) := by
+  simp [cost, eval]
+
+@[simp] theorem cost_map {T : Type t} [AddMonoid T]
+    (oracle : {ι : Type u} → F ι → ι) (weight : {ι : Type u} → F ι → T)
+    (t : FreeM F α) (f : α → β) :
+    cost oracle weight (f <$> t) = cost oracle weight t := by
+  simp [cost]
+
+/-! ### Simp lemmas for `countQueries` -/
+
+@[simp] theorem countQueries_pure (oracle : {ι : Type u} → F ι → ι) (a : α) :
+    countQueries oracle (pure a : FreeM F α) = 0 := rfl
+
+@[simp] theorem countQueries_liftBind (oracle : {ι : Type u} → F ι → ι)
+    {ι : Type u} (op : F ι) (cont : ι → FreeM F α) :
+    countQueries oracle (FreeM.lift op >>= cont) =
+      1 + countQueries oracle (cont (oracle op)) := rfl
+
+@[simp] theorem countQueries_lift (oracle : {ι : Type u} → F ι → ι)
+    {ι : Type u} (op : F ι) :
+    countQueries oracle (FreeM.lift op) = 1 :=
+  cost_lift _ _ _
+
+@[simp] theorem countQueries_bind (oracle : {ι : Type u} → F ι → ι)
+    (t : FreeM F α) (f : α → FreeM F β) :
+    countQueries oracle (t >>= f) =
+      countQueries oracle t + countQueries oracle (f (eval oracle t)) :=
+  cost_bind oracle (fun _ => 1) t f
+
+@[simp] theorem countQueries_map (oracle : {ι : Type u} → F ι → ι)
+    (t : FreeM F α) (f : α → β) :
+    countQueries oracle (f <$> t) = countQueries oracle t :=
+  cost_map oracle (fun _ => 1) t f
+
+theorem countQueries_eq_cost_one (oracle : {ι : Type u} → F ι → ι) (p : FreeM F α) :
+    countQueries oracle p = cost oracle (fun _ => 1) p := rfl
+
+@[simp↓]
+theorem countQueries_ite (oracle : {ι : Type u} → F ι → ι) (P : Prop) [Decidable P]
+    (p q : FreeM F α) :
+    (if P then p else q).countQueries oracle =
+      if P then p.countQueries oracle else q.countQueries oracle :=
+  apply_ite (countQueries oracle) P p q
+
+@[simp↓]
+theorem countQueries_dite (oracle : {ι : Type u} → F ι → ι) (P : Prop) [Decidable P]
+    (p : P → FreeM F α) (q : ¬P → FreeM F α) :
+    (if h : P then p h else q h).countQueries oracle =
+      if h : P then (p h).countQueries oracle else (q h).countQueries oracle :=
+  apply_dite (countQueries oracle) P p q
+
+/-! ## Combinatorial lower bound -/
+
+section LowerBound
+
+/-- Finset-based version: if the oracles indexed by `S` produce `|S|`-many distinct
+    evaluation results, then some oracle in `S` makes at least `⌈log_r |S|⌉` queries. -/
+private theorem exists_mem_countQueries_ge_clog (r : Nat)
+    (h_card : ∀ {ρ : Type u}, F ρ → #ρ ≤ r)
+    {ix : Type w} (p : FreeM F α) (S : Finset ix) (hS : S.Nonempty)
+    (oracles : ix → ({ρ : Type u} → F ρ → ρ))
+    (h_inj : Set.InjOn (fun i => p.eval (oracles i)) ↑S) :
+    ∃ i ∈ S, p.countQueries (oracles i) ≥ Nat.clog r S.card := by
+  classical
+  induction p generalizing ix S with
+  | pure a =>
+    obtain ⟨i, hi⟩ := hS
+    refine ⟨i, hi, ?_⟩
+    have hS1 : S.card ≤ 1 :=
+      Finset.card_le_one.mpr fun _ ha _ hb => h_inj ha hb rfl
+    simp [countQueries, Nat.clog_of_right_le_one hS1]
+  | @lift_bind ρ op cont ih =>
+    by_cases hle : S.card ≤ 1
+    · obtain ⟨i, hi⟩ := hS
+      exact ⟨i, hi, by simp [Nat.clog_of_right_le_one hle]⟩
+    push Not at hle
+    by_cases hr : r ≤ 1
+    · obtain ⟨i, hi⟩ := hS
+      exact ⟨i, hi, by simp [Nat.clog_of_left_le_one hr]⟩
+    push Not at hr
+    -- 2 ≤ r, 2 ≤ S.card
+    have : Finite ρ :=
+      Cardinal.mk_lt_aleph0_iff.mp ((h_card op).trans_lt Cardinal.natCast_lt_aleph0)
+    let _ : Fintype ρ := Fintype.ofFinite ρ
+    have hk : Fintype.card ρ ≤ r := by
+      have h := h_card op
+      rwa [Cardinal.mk_fintype, Nat.cast_le] at h
+    -- Fintype.card ρ ≥ 1: any oracle produces an answer
+    obtain ⟨i₀, _hi₀⟩ := hS
+    have : Nonempty ρ := ⟨oracles i₀ op⟩
+    have hk1 : 1 ≤ Fintype.card ρ := Fintype.card_pos
+    -- Pigeonhole: pick fiber of maximum size
+    have ⟨b, _, hb⟩ : ∃ b ∈ (Finset.univ : Finset ρ),
+        (S.card - 1) / Fintype.card ρ <
+          (S.filter (fun i => oracles i op = b)).card := by
+      apply Finset.exists_lt_card_fiber_of_mul_lt_card_of_maps_to
+        (fun a _ => Finset.mem_univ (oracles a op))
+      simp only [Finset.card_univ]
+      calc Fintype.card ρ * ((S.card - 1) / Fintype.card ρ)
+          = (S.card - 1) / Fintype.card ρ * Fintype.card ρ := Nat.mul_comm ..
+        _ ≤ S.card - 1 := Nat.div_mul_le_self _ _
+        _ < S.card := by omega
+    set S' := S.filter (fun i => oracles i op = b)
+    have hS' : S'.Nonempty :=
+      Finset.card_pos.mp (Nat.lt_of_le_of_lt (Nat.zero_le _) hb)
+    have h_inj' : Set.InjOn (fun i => (cont b).eval (oracles i)) ↑S' := by
+      intro i hi j hj heq
+      have him := Finset.mem_coe.mp hi |> Finset.mem_filter.mp
+      have hjm := Finset.mem_coe.mp hj |> Finset.mem_filter.mp
+      exact h_inj (Finset.mem_coe.mpr him.1) (Finset.mem_coe.mpr hjm.1)
+        (by simpa [FreeM.liftBind_eq, him.2, hjm.2] using heq)
+    obtain ⟨i, hi, hiq⟩ := ih b S' hS' oracles h_inj'
+    have him := Finset.mem_filter.mp hi
+    refine ⟨i, him.1, ?_⟩
+    change countQueries (oracles i) (FreeM.lift op >>= cont) ≥ Nat.clog r S.card
+    rw [countQueries_liftBind, him.2]
+    -- Need: Nat.clog r S.card ≤ 1 + (cont b).countQueries (oracles i)
+    have hS'_lb : (S.card + r - 1) / r ≤ S'.card := by
+      have h1 : (S.card - 1) / r ≤ (S.card - 1) / Fintype.card ρ :=
+        Nat.div_le_div_left hk (by omega)
+      have h2 : (S.card + r - 1) / r = (S.card - 1) / r + 1 := by
+        rw [show S.card + r - 1 = S.card - 1 + r from by omega]
+        exact Nat.add_div_right (S.card - 1) (by omega)
+      omega
+    calc Nat.clog r S.card
+        = 1 + Nat.clog r ((S.card + r - 1) / r) := by
+          rw [Nat.clog_of_two_le hr (by omega)]; omega
+      _ ≤ 1 + Nat.clog r S'.card :=
+          Nat.add_le_add_left (Nat.clog_mono_right r hS'_lb) 1
+      _ ≤ 1 + (cont b).countQueries (oracles i) := Nat.add_le_add_left hiq 1
+
+/-- If `n` oracles produce `n` distinct evaluation results from a `FreeM F α` program
+whose every response type has cardinality at most `r` (and hence is finite), then some
+oracle makes at least `⌈log_r n⌉` queries.
+
+This is the core combinatorial lemma for query complexity lower bounds. The proof uses
+the adversarial/partition argument: at each query node, the `n` oracles split by their
+answer; the largest group (size ≥ ⌈n/r⌉) still produces distinct results in the
+corresponding subtree, and the induction proceeds there. -/
+theorem exists_countQueries_ge_clog (r : Nat)
+    (h_card : ∀ {ρ : Type u}, F ρ → #ρ ≤ r)
+    (p : FreeM F α) {n : Nat}
+    (oracles : Fin n → ({ρ : Type u} → F ρ → ρ))
+    (hn : 0 < n)
+    (h_inj : Function.Injective (fun i => p.eval (oracles i))) :
+    ∃ i : Fin n, p.countQueries (oracles i) ≥ Nat.clog r n := by
+  have ⟨i, _, hi⟩ := exists_mem_countQueries_ge_clog r h_card p Finset.univ
+    (Finset.univ_nonempty_iff.mpr ⟨⟨0, hn⟩⟩) oracles h_inj.injOn
+  rw [Finset.card_univ, Fintype.card_fin] at hi
+  exact ⟨i, hi⟩
+
+end LowerBound
+
+end Cslib.FreeM
diff --git a/Cslib/Algorithms/Lean/Query/Sort/Insertion/Defs.lean b/Cslib/Algorithms/Lean/Query/Sort/Insertion/Defs.lean
new file mode 100644
index 0000000000..0d1f11e23d
--- /dev/null
+++ b/Cslib/Algorithms/Lean/Query/Sort/Insertion/Defs.lean
@@ -0,0 +1,30 @@
+/-
+Copyright (c) 2026 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Kim Morrison, Shreyas Srinivas, Eric Wieser
+-/
+module
+
+public import Cslib.Algorithms.Lean.Query.Sort.LEQuery
+public import Cslib.Algorithms.Lean.Sort.Insertion
+
+/-! # Insertion Sort as a Query Program
+
+Insertion sort implemented as a `FreeM (LEQuery α)`, making all comparison queries explicit.
+-/
+
+open Cslib Cslib.Query
+
+public section
+
+namespace Cslib.Query
+
+/-- Insert `x` into a sorted list using comparison queries. -/
+abbrev orderedInsert (x : α) (xs : List α) : FreeM (LEQuery α) (List α) :=
+  xs.orderedInsertM LEQuery.ask x
+
+/-- Sort a list using insertion sort with comparison queries. -/
+abbrev insertionSort (xs : List α) : FreeM (LEQuery α) (List α) :=
+  xs.insertionSortM LEQuery.ask
+
+end Cslib.Query
diff --git a/Cslib/Algorithms/Lean/Query/Sort/Insertion/Lemmas.lean b/Cslib/Algorithms/Lean/Query/Sort/Insertion/Lemmas.lean
new file mode 100644
index 0000000000..851ff71bbd
--- /dev/null
+++ b/Cslib/Algorithms/Lean/Query/Sort/Insertion/Lemmas.lean
@@ -0,0 +1,111 @@
+/-
+Copyright (c) 2026 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Kim Morrison, Shreyas Srinivas
+-/
+module
+
+public import Cslib.Algorithms.Lean.Query.Bounds
+public import Cslib.Algorithms.Lean.Query.Sort.IsSort
+public import Cslib.Algorithms.Lean.Query.Sort.Insertion.Defs
+public import Mathlib.Data.List.Sort
+
+/-! # Insertion Sort: Correctness and Upper Bound
+
+Proofs that `insertionSort` is a correct comparison sort and uses at most `n * (n - 1) / 2`
+queries (with `n²` as a corollary). All proofs are by plain equational reasoning on
+`FreeM.eval` and `FreeM.countQueries`.
+-/
+
+open Cslib Cslib.Query
+
+public section
+
+namespace Cslib.Query
+
+variable {α : Type}
+
+/-! ## Evaluation -/
+
+/-- Evaluating query-based insertion agrees with `List.orderedInsert` using the relation
+supplied by the oracle. -/
+@[simp] theorem eval_orderedInsert (oracle : {ι : Type} → LEQuery α ι → ι)
+    (x : α) (xs : List α) :
+    (orderedInsert x xs).eval oracle =
+      xs.orderedInsert (fun x y => oracle (.le x y)) x :=
+  Id.pure_injective <| by simp [FreeM.isMonadHom_pure_eval oracle |>.map_orderedInsertM _ x xs]
+
+/-- Evaluating query-based insertion sort agrees with `List.insertionSort` using the relation
+supplied by the oracle.
+
+This is the essential correctness statement: it identifies the query program as *the*
+insertion sort operation, so correctness properties (permutation, sortedness) transfer
+directly from the `List.insertionSort` API rather than being restated here. -/
+@[simp] theorem eval_insertionSort (oracle : {ι : Type} → LEQuery α ι → ι) (xs : List α) :
+    (insertionSort xs).eval oracle =
+      xs.insertionSort (fun x y => oracle (.le x y)) :=
+  Id.pure_injective <| by simp [FreeM.isMonadHom_pure_eval oracle |>.map_listInsertionSortM _ xs]
+
+/-! ## Query count proofs -/
+
+theorem orderedInsert_countQueries_le (oracle : {ι : Type} → LEQuery α ι → ι)
+    (x : α) (xs : List α) :
+    (orderedInsert x xs).countQueries oracle ≤ xs.length := by
+  unfold orderedInsert
+  induction xs with
+  | nil => simp
+  | cons y ys ih =>
+    simp
+    by_cases h : oracle (.le x y) = true <;> simp [h]
+    omega
+
+/-- Insertion sort makes at most `n * (n - 1) / 2` queries: inserting into the sorted
+prefix of length `k` costs at most `k` queries. This bound is attained by the all-`false`
+oracle. -/
+theorem insertionSort_countQueries_le (oracle : {ι : Type} → LEQuery α ι → ι)
+    (xs : List α) :
+    (insertionSort xs).countQueries oracle ≤ xs.length * (xs.length - 1) / 2 := by
+  induction xs with
+  | nil => simp
+  | cons x xs ih =>
+    have hq : (insertionSort (x :: xs)).countQueries oracle =
+        (insertionSort xs).countQueries oracle +
+        (orderedInsert x ((insertionSort xs).eval oracle)).countQueries oracle := by
+      simp
+    have hlen : ((insertionSort xs).eval oracle).length = xs.length := by
+      rw [eval_insertionSort]
+      exact (List.perm_insertionSort _ xs).length_eq
+    have hord := orderedInsert_countQueries_le oracle x ((insertionSort xs).eval oracle)
+    rw [hlen] at hord
+    have htri : xs.length * (xs.length - 1) / 2 + xs.length =
+        (x :: xs).length * ((x :: xs).length - 1) / 2 := by
+      rw [← Nat.choose_two_right, ← Nat.choose_two_right, List.length_cons,
+        Nat.choose_succ_succ, Nat.choose_one_right, Nat.add_comm]
+    omega
+
+theorem insertionSort_countQueries_le_sq (oracle : {ι : Type} → LEQuery α ι → ι)
+    (xs : List α) :
+    (insertionSort xs).countQueries oracle ≤ xs.length ^ 2 := by
+  have h := insertionSort_countQueries_le oracle xs
+  have h2 : xs.length * (xs.length - 1) ≤ xs.length ^ 2 := by
+    rw [Nat.pow_two]
+    exact Nat.mul_le_mul_left _ (Nat.sub_le _ _)
+  omega
+
+/-! ## UpperBound and IsSort instances -/
+
+theorem insertionSort_upperBound :
+    UpperBound (insertionSort (α := α)) List.length (· ^ 2) :=
+  UpperBound.of_pointwise (fun _ _ h => Nat.pow_le_pow_left h 2)
+    fun oracle xs => insertionSort_countQueries_le_sq oracle xs
+
+theorem insertionSort_isSort : IsSort (insertionSort (α := α)) where
+  perm xs oracle := by
+    rw [eval_insertionSort]
+    exact List.perm_insertionSort _ xs
+  sorted := by
+    intro xs oracle r _ _ _ horacle
+    rw [eval_insertionSort]
+    simpa only [horacle, decide_eq_true_eq] using List.pairwise_insertionSort r xs
+
+end Cslib.Query
diff --git a/Cslib/Algorithms/Lean/Query/Sort/IsSort.lean b/Cslib/Algorithms/Lean/Query/Sort/IsSort.lean
new file mode 100644
index 0000000000..26ad52f519
--- /dev/null
+++ b/Cslib/Algorithms/Lean/Query/Sort/IsSort.lean
@@ -0,0 +1,47 @@
+/-
+Copyright (c) 2026 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Kim Morrison, Shreyas Srinivas
+-/
+module
+
+public import Cslib.Algorithms.Lean.Query.Sort.LEQuery
+import Mathlib.Data.List.Sort
+
+/-! # IsSort: Specification for Comparison Sorts
+
+`IsSort sort` asserts that `sort` is a correct comparison sort when viewed as a `FreeM`
+over `LEQuery α`. Correctness means: for any oracle, the result is a permutation of the
+input; and for any oracle implementing a total order, the result is sorted.
+-/
+
+open Cslib Cslib.Query
+
+public section
+
+namespace Cslib.Query
+
+/-- A `FreeM`-based function is a correct comparison sort if it always produces a permutation
+    of its input, and produces a sorted list when the oracle implements a total order. -/
+structure IsSort (sort : List α → FreeM (LEQuery α) (List α)) : Prop where
+  /-- The sort produces a permutation of its input, for any oracle. -/
+  perm : ∀ (xs : List α) (oracle : {ι : Type} → LEQuery α ι → ι),
+    ((sort xs).eval oracle).Perm xs
+  /-- The sort produces a sorted list, when the oracle implements a total order. -/
+  sorted : ∀ (xs : List α) (oracle : {ι : Type} → LEQuery α ι → ι)
+    (r : α → α → Prop) [DecidableRel r] [Std.Total r] [IsTrans α r]
+    (_ : ∀ a b, oracle (.le a b) = decide (r a b)),
+    ((sort xs).eval oracle).Pairwise r
+
+/-- `IsSort` determines the output: under an oracle implementing an antisymmetric total
+    transitive relation, all correct comparison sorts produce the same list. -/
+theorem IsSort.eval_eq {sort₁ sort₂ : List α → FreeM (LEQuery α) (List α)}
+    (h₁ : IsSort sort₁) (h₂ : IsSort sort₂)
+    (r : α → α → Prop) [DecidableRel r] [Std.Total r] [IsTrans α r] [Std.Antisymm r]
+    (oracle : {ι : Type} → LEQuery α ι → ι)
+    (horacle : ∀ a b, oracle (.le a b) = decide (r a b)) (xs : List α) :
+    (sort₁ xs).eval oracle = (sort₂ xs).eval oracle :=
+  ((h₁.perm xs oracle).trans (h₂.perm xs oracle).symm).eq_of_pairwise'
+    (h₁.sorted xs oracle r horacle) (h₂.sorted xs oracle r horacle)
+
+end Cslib.Query
diff --git a/Cslib/Algorithms/Lean/Query/Sort/LEQuery.lean b/Cslib/Algorithms/Lean/Query/Sort/LEQuery.lean
new file mode 100644
index 0000000000..48a0b40efc
--- /dev/null
+++ b/Cslib/Algorithms/Lean/Query/Sort/LEQuery.lean
@@ -0,0 +1,47 @@
+/-
+Copyright (c) 2026 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Sebastian Graf, Kim Morrison, Shreyas Srinivas
+-/
+module
+
+public import Cslib.Algorithms.Lean.Query.FreeM
+
+/-! # LEQuery: Comparison Queries for Sorting
+
+`LEQuery α` is the query type for comparison-based sorting algorithms.
+A query `LEQuery.le a b` asks whether `a ≤ b` and returns a `Bool`.
+-/
+
+public section
+
+open scoped Cardinal
+
+namespace Cslib.Query
+
+/-- Comparison query: asks whether `a ≤ b`, returning a `Bool`. -/
+inductive LEQuery (α : Type) : Type → Type where
+  | le (a b : α) : LEQuery α Bool
+
+/-- Lift `LEQuery.le a b` into a `FreeM` that returns the comparison result. -/
+abbrev LEQuery.ask (a b : α) : FreeM (LEQuery α) Bool :=
+  FreeM.lift (.le a b)
+
+@[simp] theorem LEQuery.eval_ask (oracle : {ι : Type} → LEQuery α ι → ι) (a b : α) :
+    (LEQuery.ask a b).eval oracle = oracle (.le a b) := rfl
+
+/-- Build an oracle for `LEQuery α` from a binary predicate `α → α → Bool`. -/
+@[expose] def LEQuery.oracleOf (f : α → α → Bool) : {ι : Type} → LEQuery α ι → ι
+  | _, .le a b => f a b
+
+@[simp] theorem LEQuery.oracleOf_le (f : α → α → Bool) (a b : α) :
+    LEQuery.oracleOf f (.le a b) = f a b := rfl
+
+/-- Every `LEQuery α ι` has response type `ι = Bool`, of cardinality two. -/
+theorem LEQuery.cardResponse_eq_two : ∀ {ι : Type}, LEQuery α ι → #ι = 2
+  | _, .le _ _ => Cardinal.mk_bool
+
+theorem LEQuery.cardResponse_le_two {ι : Type} (op : LEQuery α ι) : #ι ≤ 2 :=
+  (LEQuery.cardResponse_eq_two op).le
+
+end Cslib.Query
diff --git a/Cslib/Algorithms/Lean/Query/Sort/LowerBound.lean b/Cslib/Algorithms/Lean/Query/Sort/LowerBound.lean
new file mode 100644
index 0000000000..dd9346f10c
--- /dev/null
+++ b/Cslib/Algorithms/Lean/Query/Sort/LowerBound.lean
@@ -0,0 +1,157 @@
+/-
+Copyright (c) 2026 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Kim Morrison, Shreyas Srinivas, Eric Wieser
+-/
+module
+
+public import Cslib.Algorithms.Lean.Query.Bounds
+public import Cslib.Algorithms.Lean.Query.Sort.IsSort
+public import Mathlib.Data.List.Sort
+public import Mathlib.Data.Nat.Factorial.Basic
+public import Mathlib.Data.Fintype.Perm
+public import Mathlib.Data.List.FinRange
+public import Mathlib.SetTheory.Cardinal.Order
+
+/-! # Comparison Sorting Lower Bound
+
+`IsSort.lowerBound_infinite`: any correct comparison sort on an infinite type
+has query complexity at least `⌈log₂(n!)⌉` for every input size `n`.
+
+The proof constructs `n!` distinct total orders on `α` (one per permutation of `n`
+embedded elements), shows they produce distinct sorted outputs, and applies
+`FreeM.exists_countQueries_ge_clog` with `LEQuery.cardResponse_le_two` witnessing that
+all responses come from `Bool` (cardinality 2).
+-/
+
+open Cslib Cslib.Query
+
+public section
+
+-- Proposed upstream in https://github.com/leanprover-community/mathlib4/pull/43326;
+-- remove once cslib's Mathlib includes it.
+private instance [Std.Total r] : Std.Total (InvImage r f) where
+  total x y := Std.Total.total (f x) (f y)
+
+namespace Cslib.Query
+
+/-! ## PrefixPermOrder: constructing n! distinct total orders -/
+
+open scoped Cardinal
+
+variable {n : ℕ}
+
+/-- A constrained version of `Infinite.natEmbedding`. -/
+private noncomputable def finEmbedding (h : n ≤ #α) : Fin n ↪ α :=
+  Nonempty.some <| by rwa [← Cardinal.le_def, Cardinal.mk_fin]
+
+/-- Distinguish `n` elements of a type. -/
+private noncomputable def finPrefix (h : ↑n ≤ #α) : α → Fin n ⊕ α :=
+  Function.extend (finEmbedding h) .inl .inr
+
+@[simp, grind =] private lemma finPrefix_natEmbedding_finVal (h : n ≤ #α) (i : Fin n) :
+    finPrefix h (finEmbedding h i) = .inl i :=
+  (finEmbedding h).injective.extend_apply _ _ _
+
+private theorem finPrefix_injective (h : ↑n ≤ #α) :
+    Function.Injective (finPrefix h) :=
+  (finEmbedding h).injective.extend_of_disjoint Sum.inl_injective Sum.inr_injective
+    Set.isCompl_range_inl_range_inr.disjoint
+
+/-- A total order on an type `α` with at least `n` elements, that orders `n` embedded elements
+    (via `finEmbedding) according to `σ⁻¹`, with embedded elements
+    preceding all others, and a well-ordering among non-embedded elements. -/
+private noncomputable def PrefixPermOrder (h : ↑n ≤ #α)
+    (σ : Equiv.Perm (Fin n)) : α → α → Prop :=
+  letI := IsWellOrder.linearOrder (α := α) WellOrderingRel
+  InvImage (Sum.Lex (InvImage (· ≤ ·) σ.symm) (· ≤ ·)) (finPrefix h)
+
+private noncomputable instance (h : ↑n ≤ #α) :
+    DecidableRel (PrefixPermOrder h σ) := Classical.decRel _
+
+private instance (h : ↑n ≤ #α) :
+    IsTrans α (PrefixPermOrder h σ) := by
+  unfold PrefixPermOrder
+  infer_instance
+
+private instance (h : ↑n ≤ #α) :
+    Std.Total (PrefixPermOrder h σ) := by
+  unfold PrefixPermOrder
+  infer_instance
+
+private instance (h : ↑n ≤ #α) :
+    Std.Antisymm (PrefixPermOrder h σ) := by
+  have : Std.Antisymm (InvImage (· ≤ ·) σ.symm) := σ.symm.injective.antisymm_onFun _
+  exact finPrefix_injective h |>.antisymm_onFun _
+
+/-- `PrefixPermOrder` restricted to embedded values matches `σ⁻¹(·) ≤ σ⁻¹(·)`. -/
+@[grind =]
+private theorem PrefixPermOrder_on_embedded (h : ↑n ≤ #α) {i j : Fin n} :
+    PrefixPermOrder h σ (finEmbedding h i) (finEmbedding h j) ↔ σ.symm i ≤ σ.symm j := by
+  simp [PrefixPermOrder, InvImage]
+
+/-- `map (ι ∘ σ) (finRange n)` is pairwise sorted by `PrefixPermOrder n σ`. -/
+private theorem pairwise_map_PrefixPermOrder (h : ↑n ≤ #α) (σ : Equiv.Perm (Fin n)) :
+    List.Pairwise (PrefixPermOrder h σ)
+      ((List.finRange n).map (fun i => finEmbedding h (σ i))) := by
+  rw [List.pairwise_map]
+  exact (List.pairwise_le_finRange n).imp fun hab => by grind
+
+/-- `map (ι ∘ σ) (finRange n)` is a permutation of `map ι (finRange n)`. -/
+private theorem map_perm_of_finEmbedding (h : ↑n ≤ #α) (σ : Equiv.Perm (Fin n)) :
+    ((List.finRange n).map (fun i => finEmbedding h (σ i))).Perm
+      ((List.finRange n).map (fun i => finEmbedding h i)) := by
+  rw [show (fun i => finEmbedding h (σ i)) =
+      (fun i => finEmbedding h i) ∘ σ from rfl]
+  grind [Equiv.Perm.map_finRange_perm]
+
+/-- Different permutations give different `map (ι ∘ σ) (finRange n)`. -/
+private theorem map_finEmbedding_injective (h : ↑n ≤ #α) :
+    Function.Injective (fun σ : Equiv.Perm (Fin n) =>
+      (List.finRange n).map (fun i => finEmbedding h (σ i))) := by
+  intro σ τ h
+  ext i
+  have := List.map_inj_left.mp h i (List.mem_finRange i)
+  grind
+
+/-! ## Main theorem -/
+
+/-- Any correct comparison sort on an infinite type has query complexity at least `⌈log₂(n!)⌉`
+    for every input size `n`. -/
+theorem IsSort.lowerBound_infinite [Infinite α]
+    {sort : List α → FreeM (LEQuery α) (List α)}
+    (hs : IsSort sort) :
+    LowerBound sort List.length (fun n => Nat.clog 2 (Nat.factorial n)) := by
+  intro n
+  have h : n ≤ #α := by
+    grw [Cardinal.natCast_le_aleph0, ← Cardinal.infinite_iff]
+    infer_instance
+  set ι := finEmbedding h
+  refine ⟨(List.finRange n).map ι, by simp, ?_⟩
+  set xs := (List.finRange n).map ι
+  have hcard : Fintype.card (Equiv.Perm (Fin n)) = Nat.factorial n := by
+    rw [Fintype.card_perm, Fintype.card_fin]
+  let e := Fintype.equivFinOfCardEq hcard
+  let progOracles : Fin (Nat.factorial n) → ({ι : Type} → LEQuery α ι → ι) :=
+    fun i => LEQuery.oracleOf fun a b => decide (PrefixPermOrder h (e.symm i) a b)
+  -- Each oracle produces a unique sorted output
+  have eval_eq_map (i) : (sort xs).eval (progOracles i) =
+      (List.finRange n).map (fun k => ι (e.symm i k)) := by
+    have h_perm := hs.perm xs (progOracles i)
+    have h_sorted := hs.sorted xs (progOracles i)
+      (PrefixPermOrder h (e.symm i))
+      (fun a b => by simp [progOracles])
+    exact h_perm.trans (map_perm_of_finEmbedding h (e.symm i)).symm |>.eq_of_pairwise'
+      h_sorted (pairwise_map_PrefixPermOrder h (e.symm i))
+  have h_inj : Function.Injective (fun i => (sort xs).eval (progOracles i)) := by
+    intro i j h_eval
+    dsimp only at h_eval
+    rw [eval_eq_map, eval_eq_map] at h_eval
+    exact e.symm.injective (map_finEmbedding_injective h h_eval)
+  -- Apply the FreeM lower-bound lemma directly
+  obtain ⟨i, hi⟩ := FreeM.exists_countQueries_ge_clog 2
+    LEQuery.cardResponse_le_two
+    (sort xs) progOracles (Nat.factorial_pos n) h_inj
+  exact ⟨progOracles i, hi⟩
+
+end Cslib.Query
diff --git a/Cslib/Algorithms/Lean/Query/Sort/Merge/Bounds.lean b/Cslib/Algorithms/Lean/Query/Sort/Merge/Bounds.lean
new file mode 100644
index 0000000000..5af96deb39
--- /dev/null
+++ b/Cslib/Algorithms/Lean/Query/Sort/Merge/Bounds.lean
@@ -0,0 +1,38 @@
+/-
+Copyright (c) 2026 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Kim Morrison
+-/
+module
+
+public import Cslib.Algorithms.Lean.Query.Sort.LowerBound
+public import Cslib.Algorithms.Lean.Query.Sort.Merge.Lemmas
+
+/-! # Merge Sort: Combined Bounds
+
+Instantiating the general comparison-sorting lower bound at `mergeSort`, and comparing it
+with the `n * ⌈log₂ n⌉` upper bound. Since `LowerBound.le_upperBound` makes the two
+bounds meet, the purely arithmetic fact `⌈log₂ n!⌉ ≤ n * ⌈log₂ n⌉` falls out of the
+framework with no further work.
+-/
+
+open Cslib Cslib.Query
+
+public section
+
+namespace Cslib.Query
+
+variable {α : Type}
+
+/-- Merge sort has worst-case query complexity at least `⌈log₂(n!)⌉`. -/
+theorem mergeSort_lowerBound [Infinite α] :
+    LowerBound (mergeSort (α := α)) List.length (fun n => Nat.clog 2 (Nat.factorial n)) :=
+  mergeSort_isSort.lowerBound_infinite
+
+/-- Sanity check that the bounds compose: comparing merge sort's upper and lower bounds
+    yields this arithmetic fact with no further work. -/
+theorem clog_factorial_le_mul_clog (n : ℕ) :
+    Nat.clog 2 (Nat.factorial n) ≤ n * Nat.clog 2 n :=
+  (mergeSort_lowerBound (α := ℕ)).le_upperBound mergeSort_upperBound n
+
+end Cslib.Query
diff --git a/Cslib/Algorithms/Lean/Query/Sort/Merge/Defs.lean b/Cslib/Algorithms/Lean/Query/Sort/Merge/Defs.lean
new file mode 100644
index 0000000000..f5ab732fb3
--- /dev/null
+++ b/Cslib/Algorithms/Lean/Query/Sort/Merge/Defs.lean
@@ -0,0 +1,72 @@
+/-
+Copyright (c) 2026 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Kim Morrison, Shreyas Srinivas, Sorrachai Yingchareonthawornchai
+-/
+module
+
+public import Cslib.Algorithms.Lean.Query.Sort.LEQuery
+public import Cslib.Algorithms.Lean.Sort.Merge
+import all Init.Data.List.Sort.Basic
+import all Cslib.Algorithms.Lean.Sort.Merge
+
+/-! # Merge Sort as a Query Program
+
+Merge sort implemented as a `FreeM (LEQuery α)`, making all comparison queries explicit.
+The definitions mirror `List.merge` and `List.mergeSort` exactly: the list is split into
+contiguous halves and the merge prefers the left element on ties. Consequently evaluating
+the query program against any oracle produces literally the same list as `List.mergeSort`
+with the comparator induced by the oracle (`eval_mergeSort` in
+`Cslib.Algorithms.Lean.Query.Sort.Merge.Lemmas`); in particular the sort is stable.
+The recursive calls of `mergeSort` are not structural, since the two halves are not
+syntactic subterms, and are justified separately using their lengths.
+-/
+
+open Cslib Cslib.Query
+
+public section
+
+namespace List
+
+/-- Split a list into contiguous halves; if the length is odd, the first half is one element
+longer. This agrees with `List.MergeSort.Internal.splitInTwo`, so that `mergeSort` agrees
+with `List.mergeSort`. -/
+@[expose] def split (xs : List α) : List α × List α :=
+  (xs.take ((xs.length + 1) / 2), xs.drop ((xs.length + 1) / 2))
+
+@[simp] theorem split_fst_length_eq (xs : List α) :
+    (split xs).1.length = (xs.length + 1) / 2 := by
+  simp [split]
+  omega
+
+@[simp] theorem split_snd_length_eq (xs : List α) :
+    (split xs).2.length = xs.length / 2 := by
+  simp [split]
+  omega
+
+theorem split_fst_append_split_snd (xs : List α) : (split xs).1 ++ (split xs).2 = xs :=
+  List.take_append_drop _ xs
+
+variable [Monad m] (cmp : α → α → m Bool)
+
+theorem splitInTwo_fst (xs : {l : List α // l.length = n}) :
+    (List.MergeSort.Internal.splitInTwo xs).1 = xs.val.split.1 := by
+  simp [split, xs.prop]
+
+theorem splitInTwo_snd (xs : {l : List α // l.length = n}) :
+    (List.MergeSort.Internal.splitInTwo xs).2 = xs.val.split.2 := by
+  simp [split, xs.prop]
+
+end List
+
+namespace Cslib.Query
+
+/-- Merge two sorted lists using comparison queries. -/
+abbrev merge (xs ys : List α) : FreeM (LEQuery α) (List α) :=
+  xs.mergeM ys LEQuery.ask
+
+/-- Sort a list using merge sort with comparison queries. -/
+abbrev mergeSort (xs : List α) : FreeM (LEQuery α) (List α) :=
+  xs.mergeSortM LEQuery.ask
+
+end Cslib.Query
diff --git a/Cslib/Algorithms/Lean/Query/Sort/Merge/Lemmas.lean b/Cslib/Algorithms/Lean/Query/Sort/Merge/Lemmas.lean
new file mode 100644
index 0000000000..2d4ab4820e
--- /dev/null
+++ b/Cslib/Algorithms/Lean/Query/Sort/Merge/Lemmas.lean
@@ -0,0 +1,179 @@
+/-
+Copyright (c) 2026 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Kim Morrison, Shreyas Srinivas, Sorrachai Yingchareonthawornchai
+-/
+module
+
+public import Cslib.Algorithms.Lean.Query.Bounds
+public import Cslib.Algorithms.Lean.Query.Sort.IsSort
+public import Cslib.Algorithms.Lean.Query.Sort.Merge.Defs
+public import Mathlib.Data.Nat.Log
+import all Init.Data.List.Sort.Basic
+import all Cslib.Algorithms.Lean.Sort.Merge
+
+/-! # Merge Sort: Correctness and Upper Bound
+
+Proofs that `mergeSort` is a correct comparison sort and uses at most `n * ⌈log₂ n⌉` queries.
+
+`eval_mergeSort` identifies the query program with `List.mergeSort`: evaluating against any
+oracle produces the same list as `List.mergeSort` with the comparator induced by the oracle.
+Correctness properties (permutation, sortedness) transfer directly from the `List.mergeSort`
+API. The query bound is proved by equational reasoning on `FreeM.countQueries`, which has no
+`List` counterpart.
+-/
+
+open Cslib Cslib.Query
+open scoped List
+
+public section
+
+namespace Cslib.Query
+
+variable {α : Type}
+
+/-! ## Evaluation -/
+
+/-- Evaluating the query-based merge agrees with `List.merge` using the relation supplied
+by the oracle. -/
+@[simp] theorem eval_merge (oracle : {ι : Type} → LEQuery α ι → ι) (xs ys : List α) :
+    (merge xs ys).eval oracle = xs.merge ys (fun a b => oracle (.le a b)) :=
+  Id.pure_injective <| by simp [FreeM.isMonadHom_pure_eval oracle |>.map_listMergeM xs ys]
+
+/-- Evaluating query-based merge sort agrees with `List.mergeSort` using the relation
+supplied by the oracle.
+
+This is the essential correctness statement: it identifies the query program as *the*
+merge sort operation, so correctness properties (permutation, sortedness, stability)
+transfer directly from the `List.mergeSort` API rather than being restated here. -/
+@[simp] theorem eval_mergeSort (oracle : {ι : Type} → LEQuery α ι → ι) (xs : List α) :
+    (mergeSort xs).eval oracle = xs.mergeSort (fun a b => oracle (.le a b)) :=
+  Id.pure_injective <| by simp [FreeM.isMonadHom_pure_eval oracle |>.map_listMergeSortM xs]
+
+/-! ## Correctness, transferred from the `List.mergeSort` API -/
+
+theorem mergeSort_perm (oracle : {ι : Type} → LEQuery α ι → ι) (xs : List α) :
+    (mergeSort xs).eval oracle ~ xs := by
+  rw [eval_mergeSort]
+  exact List.mergeSort_perm xs _
+
+theorem mergeSort_sorted
+    (r : α → α → Prop) [DecidableRel r] [Std.Total r] [IsTrans α r]
+    (oracle : {ι : Type} → LEQuery α ι → ι)
+    (horacle : ∀ a b, oracle (.le a b) = decide (r a b))
+    (xs : List α) :
+    ((mergeSort xs).eval oracle).Pairwise r := by
+  rw [eval_mergeSort]
+  refine (List.pairwise_mergeSort ?_ ?_ xs).imp (by simp [horacle])
+  · intro a b c hab hbc
+    simp only [horacle, decide_eq_true_eq] at hab hbc ⊢
+    exact _root_.trans hab hbc
+  · intro a b
+    simp only [horacle, Bool.or_eq_true, decide_eq_true_eq]
+    exact Std.Total.total a b
+
+/-! ## Query count simp lemmas -/
+
+theorem countQueries_merge_nil_left (oracle : {ι : Type} → LEQuery α ι → ι) (ys : List α) :
+    (merge ([] : List α) ys).countQueries oracle = 0 := by
+  simp
+
+theorem countQueries_merge_nil_right (oracle : {ι : Type} → LEQuery α ι → ι) (xs : List α) :
+    (merge xs ([] : List α)).countQueries oracle = 0 := by
+  simp
+
+theorem countQueries_merge_cons_cons (oracle : {ι : Type} → LEQuery α ι → ι)
+    (x : α) (xs' : List α) (y : α) (ys' : List α) :
+    (merge (x :: xs') (y :: ys')).countQueries oracle =
+      1 + if oracle (.le x y)
+      then (merge xs' (y :: ys')).countQueries oracle
+      else (merge (x :: xs') ys').countQueries oracle := by
+  simp
+
+theorem countQueries_mergeSort_nil (oracle : {ι : Type} → LEQuery α ι → ι) :
+    (mergeSort (α := α) []).countQueries oracle = 0 := by
+  simp
+
+theorem countQueries_mergeSort_singleton (oracle : {ι : Type} → LEQuery α ι → ι) (x : α) :
+    (mergeSort [x]).countQueries oracle = 0 := by
+  simp
+
+open List (split) in
+@[simp] theorem countQueries_mergeSort_cons_cons (oracle : {ι : Type} → LEQuery α ι → ι)
+    (x y : α) (zs : List α) :
+    (mergeSort (x :: y :: zs)).countQueries oracle =
+      (mergeSort (x :: y :: zs).split.1).countQueries oracle +
+      ((mergeSort (x :: y :: zs).split.2).countQueries oracle +
+       (merge ((x :: y :: zs).split.1.mergeSort fun a b => oracle (.le a b))
+              ((x :: y :: zs).split.2.mergeSort fun a b => oracle (.le a b))).countQueries
+         oracle) := by
+  simp only [List.mergeSortM, List.splitInTwo_fst, List.splitInTwo_snd]
+  simp
+
+/-! ## Query count proofs -/
+
+theorem merge_countQueries_le (oracle : {ι : Type} → LEQuery α ι → ι)
+    (xs ys : List α) :
+    (merge xs ys).countQueries oracle ≤ xs.length + ys.length := by
+  induction xs, ys using List.mergeM.induct (α := α) with
+  | case1 ys => simp
+  | case2 xs => simp
+  | case3 x xs' y ys' ih_true ih_false =>
+    simp only [countQueries_merge_cons_cons, List.length_cons]
+    split <;> simp_all <;> omega
+
+/-- The key arithmetic inequality for the merge sort recurrence:
+    `⌈n/2⌉ * clog(⌈n/2⌉) + ⌊n/2⌋ * clog(⌊n/2⌋) + n ≤ n * clog(n)`. -/
+private theorem mergeSort_bound (n : ℕ) (hn : 2 ≤ n) :
+    ((n + 1) / 2) * Nat.clog 2 ((n + 1) / 2) +
+      (n / 2 * Nat.clog 2 (n / 2) + ((n + 1) / 2 + n / 2)) ≤
+      n * Nat.clog 2 n := by
+  have hclog := Nat.clog_of_one_lt (by omega : (1 : Nat) < 2) hn
+  have hceil : Nat.clog 2 ((n + 1) / 2) + 1 ≤ Nat.clog 2 n := le_of_eq hclog.symm
+  have hfloor : Nat.clog 2 (n / 2) + 1 ≤ Nat.clog 2 n :=
+    (Nat.add_le_add_right (Nat.clog_mono_right 2 (by omega)) 1).trans hceil
+  have hsum : (n + 1) / 2 + n / 2 = n := by omega
+  have h1 := Nat.mul_le_mul_left ((n + 1) / 2) hceil
+  have h2 := Nat.mul_le_mul_left (n / 2) hfloor
+  rw [Nat.mul_succ] at h1 h2
+  calc _ = ((n + 1) / 2 * Nat.clog 2 ((n + 1) / 2) + (n + 1) / 2) +
+           (n / 2 * Nat.clog 2 (n / 2) + n / 2) := by omega
+    _ ≤ (n + 1) / 2 * Nat.clog 2 n + n / 2 * Nat.clog 2 n := Nat.add_le_add h1 h2
+    _ = ((n + 1) / 2 + n / 2) * Nat.clog 2 n := (Nat.add_mul ..).symm
+    _ = n * Nat.clog 2 n := by rw [hsum]
+
+theorem mergeSort_countQueries_le (oracle : {ι : Type} → LEQuery α ι → ι)
+    (xs : List α) :
+    (mergeSort xs).countQueries oracle ≤ xs.length * Nat.clog 2 xs.length := by
+  induction xs using List.mergeSortM.induct (α := α) with
+  | case1 => simp [mergeSort]
+  | case2 x => simp [mergeSort]
+  | case3 x y zs halves ih_l ih_r =>
+    subst halves
+    simp only [List.splitInTwo_fst, List.splitInTwo_snd] at ih_l ih_r
+    simp only [countQueries_mergeSort_cons_cons]
+    have hml := merge_countQueries_le oracle
+      ((x :: y :: zs).split.1.mergeSort fun a b => oracle (.le a b))
+      ((x :: y :: zs).split.2.mergeSort fun a b => oracle (.le a b))
+    rw [List.length_mergeSort, List.length_mergeSort,
+        List.split_fst_length_eq, List.split_snd_length_eq] at hml
+    rw [List.split_fst_length_eq] at ih_l
+    rw [List.split_snd_length_eq] at ih_r
+    exact Nat.le_trans (Nat.add_le_add ih_l (Nat.add_le_add ih_r hml))
+      (mergeSort_bound _ (by simp only [List.length_cons]; omega))
+
+/-! ## UpperBound and IsSort instances -/
+
+theorem mergeSort_upperBound :
+    UpperBound (mergeSort (α := α)) List.length (fun n => n * Nat.clog 2 n) :=
+  UpperBound.of_pointwise
+    (fun _ _ h => Nat.mul_le_mul h (Nat.clog_mono_right 2 h))
+    fun oracle xs => mergeSort_countQueries_le oracle xs
+
+theorem mergeSort_isSort : IsSort (mergeSort (α := α)) where
+  perm xs oracle := mergeSort_perm oracle xs
+  sorted := by
+    intro xs oracle r _ _ _ horacle
+    exact mergeSort_sorted r oracle horacle xs
+
+end Cslib.Query
diff --git a/Cslib/Foundations/Control/Monad/Free.lean b/Cslib/Foundations/Control/Monad/Free.lean
index 74dea4913c..90ca3712af 100644
--- a/Cslib/Foundations/Control/Monad/Free.lean
+++ b/Cslib/Foundations/Control/Monad/Free.lean
@@ -262,7 +262,7 @@ theorem isMonadHom_liftM [LawfulMonad m] (interp : {ι : Type u} → F ι → m
 @[simp]
 lemma liftM_map [LawfulMonad m]
     (interp : {ι : Type u} → F ι → m ι) (f : α → β) (x : FreeM F α) :
-    (f <$> x).liftM interp = f <$> x.liftM interp :=
+    (f <$> x).liftM @interp = f <$> x.liftM @interp :=
   isMonadHom_liftM interp |>.map_map _ _
 
 @[simp]
diff --git a/Cslib/Foundations/Control/Monad/IsMonadHom.lean b/Cslib/Foundations/Control/Monad/IsMonadHom.lean
index a515d1a408..a2633772bd 100644
--- a/Cslib/Foundations/Control/Monad/IsMonadHom.lean
+++ b/Cslib/Foundations/Control/Monad/IsMonadHom.lean
@@ -24,6 +24,11 @@ operators when the structures are lawful.
 
 public section
 
+-- Missing from core
+
+theorem _root_.Id.pure_injective : Function.Injective (pure : α → Id α) :=
+  fun _ _ => Id.ext_iff.1
+
 namespace Cslib
 
 /-! ### Functor Homomorphisms -/
diff --git a/CslibTests.lean b/CslibTests.lean
index 64e84ecbe9..4d938d2244 100644
--- a/CslibTests.lean
+++ b/CslibTests.lean
@@ -22,5 +22,6 @@ import CslibTests.Modal.Ideal
 import CslibTests.Modal.Stlc
 import CslibTests.MultiTapeComplexity
 import CslibTests.PACLearning
+import CslibTests.Query
 import CslibTests.Reduction
 import CslibTests.StatefulProcesses
diff --git a/CslibTests/Query.lean b/CslibTests/Query.lean
new file mode 100644
index 0000000000..3bf030d338
--- /dev/null
+++ b/CslibTests/Query.lean
@@ -0,0 +1,59 @@
+/-
+Copyright (c) 2026 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Kim Morrison
+-/
+import Cslib.Algorithms.Lean.Query.Sort.Merge.Bounds
+import Cslib.Algorithms.Lean.Query.Sort.Insertion.Lemmas
+import Cslib.Algorithms.Lean.Query.Arith.Lemmas
+
+/-! # Tests for the query complexity framework
+
+Executable checks that the query programs compute, plus compile-time checks exercising
+the public API (bound combinators, sort uniqueness, universe polymorphism).
+-/
+
+set_option linter.hashCommand false
+
+open Cslib Cslib.Query
+
+/-- The honest comparison oracle on `ℕ`. -/
+def leOracle : {ι : Type} → LEQuery ℕ ι → ι :=
+  LEQuery.oracleOf fun a b => decide (a ≤ b)
+
+-- The query sorts compute, and agree with the reference sorts.
+#guard (mergeSort [3, 1, 2]).eval leOracle == [1, 2, 3]
+#guard (insertionSort [3, 1, 2]).eval leOracle == [1, 2, 3]
+
+-- Query counts along the honest path.
+#guard (mergeSort [3, 1, 2]).countQueries leOracle == 3
+#guard (insertionSort [3, 1, 2]).countQueries leOracle == 3
+
+-- The sharp insertion bound `n * (n - 1) / 2` is attained by the all-`false` oracle.
+#guard (insertionSort [1, 2, 3]).countQueries (LEQuery.oracleOf fun _ _ => false) == 3
+
+-- `mergeSort` is stable: with equal keys, payloads keep their input order.
+#guard (mergeSort [(1, "b"), (0, "x"), (1, "a")]).eval
+    (LEQuery.oracleOf fun p q => decide (p.1 ≤ q.1)) == [(0, "x"), (1, "b"), (1, "a")]
+
+-- The complex multiplication examples compute.
+#guard (complexMulNaive (1 : Int) 2 3 4).eval ArithQuery.honest == (-5, 10)
+#guard (complexMulGauss (1 : Int) 2 3 4).eval ArithQuery.honest == (-5, 10)
+
+-- All correct comparison sorts agree under a linear-order oracle (`IsSort.eval_eq`).
+example (xs : List ℕ) :
+    (mergeSort xs).eval leOracle = (insertionSort xs).eval leOracle :=
+  mergeSort_isSort.eval_eq insertionSort_isSort (· ≤ ·) leOracle (fun _ _ => rfl) xs
+
+-- The sharp triangular bound for insertion sort.
+example (oracle : {ι : Type} → LEQuery ℕ ι → ι) (xs : List ℕ) :
+    (insertionSort xs).countQueries oracle ≤ xs.length * (xs.length - 1) / 2 :=
+  insertionSort_countQueries_le oracle xs
+
+-- Upper and lower bounds compose via `LowerBound.le_upperBound`.
+example (n : ℕ) : Nat.clog 2 (Nat.factorial n) ≤ n * Nat.clog 2 n :=
+  (mergeSort_lowerBound (α := ℕ)).le_upperBound mergeSort_upperBound n
+
+-- `UpperBound` is universe polymorphic in the query family.
+example (Q : Type 1 → Type 2) (prog : Bool → FreeM Q PUnit.{2}) : Prop :=
+  UpperBound prog (fun _ => 0) id