diff --git a/Complexity.lean b/Complexity.lean
index 80ab96083..c9bd5bb86 100644
--- a/Complexity.lean
+++ b/Complexity.lean
@@ -32,6 +32,10 @@ public import Complexity.Algorithms.Reachability.InductiveCounting.Semantics
 public import Complexity.Algorithms.Reachability.Reingold
 public import Complexity.Algorithms.Reachability.ReingoldEval
 public import Complexity.Algorithms.Reachability.Savitch
+public import Complexity.Algorithms.Streaming.CountMin.Basic
+public import Complexity.Algorithms.Streaming.CountMin.LinearHash
+public import Complexity.Algorithms.Streaming.CountMin.Probability
+public import Complexity.Algorithms.Streaming.CountMin.Program
 public import Complexity.Algorithms.WordRAM.DynamicArray
 public import Complexity.Algorithms.WordRAM.ElementDistinctness
 public import Complexity.Algorithms.WordRAM.ElementDistinctnessRAM
diff --git a/Complexity/Algorithms/Streaming/CountMin/Basic.lean b/Complexity/Algorithms/Streaming/CountMin/Basic.lean
new file mode 100644
index 000000000..5e0c4b2c3
--- /dev/null
+++ b/Complexity/Algorithms/Streaming/CountMin/Basic.lean
@@ -0,0 +1,244 @@
+/-
+Copyright (c) 2026 Samuel Schlesinger. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Samuel Schlesinger
+-/
+
+module
+-- upstream: candidate
+
+public import Complexity.Init
+public import Mathlib.Algebra.BigOperators.Group.List.Basic
+public import Mathlib.Data.Finset.Lattice.Fold
+public import Mathlib.Data.Fintype.Fin
+public import Init.Data.Vector.Lemmas
+public import Init.Data.Vector.OfFn
+
+/-!
+# Count-Min sketches for weighted insertion streams
+
+An update `(x, c)` adds the natural-number weight `c` to one bucket in each hash row. The
+counter table is a vector of vectors, so updates materialize a finite table instead of retaining
+a chain of functional updates. A point query takes the minimum of the counters addressed by
+the queried item. It never underestimates the true frequency.
+
+The exact bucket invariant identifies this executable update-and-fold algorithm with sums of
+stream weights. Tables built with the same hashes merge by entrywise addition. Every counter is
+bounded by the total inserted weight. These are semantic and numerical guarantees; this module
+does not assign machine running times to Lean operations or certify their heap consumption.
+
+## Main definitions
+
+* `Cslib.CountMin.frequency`, `Cslib.CountMin.mass`: weighted frequency and total stream mass.
+* `Cslib.CountMin.bucket`, `Cslib.CountMin.noise`: exact bucket and collision sums.
+* `Cslib.CountMin.Table`, `Cslib.CountMin.update`, `Cslib.CountMin.run`: stored counters and
+  the executable streaming algorithm.
+* `Cslib.CountMin.estimate`: the minimum of a nonempty collection of hash rows.
+* `Cslib.CountMin.merge`: entrywise addition of tables using the same hashes.
+
+## Main results
+
+* `Cslib.CountMin.bucket_hash_eq_frequency_add_noise`: a queried counter is frequency plus noise.
+* `Cslib.CountMin.run_get`: every stored counter equals its bucket sum.
+* `Cslib.CountMin.frequency_le_estimate_run`: no underestimation.
+* `Cslib.CountMin.run_get_le_mass`: each counter is at most the total stream weight.
+* `Cslib.CountMin.run_append`: concatenation of streams agrees with merging their tables.
+
+## References
+
+* [G. Cormode, S. Muthukrishnan, *An Improved Data Stream Summary: The Count-Min Sketch and its
+  Applications*, Sections 3 and 4.1][CormodeMuthukrishnan2005]
+-/
+
+@[expose] public section
+
+namespace Cslib.CountMin
+
+variable {X : Type*} {d w : ℕ}
+
+/-- Total weight inserted by a stream. -/
+def mass (s : List (X × ℕ)) : ℕ := (s.map Prod.snd).sum
+
+/-- Total weight inserted at the queried item. -/
+def frequency [DecidableEq X] (s : List (X × ℕ)) (x : X) : ℕ :=
+  (s.map fun u => if u.1 = x then u.2 else 0).sum
+
+/-- The weight in one bucket of a hash row. -/
+def bucket (h : X → Fin w) (s : List (X × ℕ)) (b : Fin w) : ℕ :=
+  (s.map fun u => if h u.1 = b then u.2 else 0).sum
+
+/-- Weight contributed by other items colliding with the query in one hash row. -/
+def noise [DecidableEq X] (h : X → Fin w) (s : List (X × ℕ)) (x : X) : ℕ :=
+  (s.map fun u => if u.1 ≠ x ∧ h u.1 = h x then u.2 else 0).sum
+
+@[simp] theorem mass_nil : mass ([] : List (X × ℕ)) = 0 := rfl
+
+@[simp] theorem mass_cons (u : X × ℕ) (s : List (X × ℕ)) :
+    mass (u :: s) = u.2 + mass s := by simp [mass]
+
+@[simp] theorem frequency_nil [DecidableEq X] (x : X) : frequency [] x = 0 := rfl
+
+@[simp] theorem frequency_cons [DecidableEq X] (u : X × ℕ) (s : List (X × ℕ)) (x : X) :
+    frequency (u :: s) x = (if u.1 = x then u.2 else 0) + frequency s x := by
+  simp [frequency]
+
+@[simp] theorem bucket_nil (h : X → Fin w) (b : Fin w) : bucket h [] b = 0 := rfl
+
+@[simp] theorem bucket_cons (h : X → Fin w) (u : X × ℕ) (s : List (X × ℕ)) (b : Fin w) :
+    bucket h (u :: s) b = (if h u.1 = b then u.2 else 0) + bucket h s b := by
+  simp [bucket]
+
+@[simp] theorem noise_nil [DecidableEq X] (h : X → Fin w) (x : X) : noise h [] x = 0 := rfl
+
+@[simp] theorem noise_cons [DecidableEq X] (h : X → Fin w) (u : X × ℕ)
+    (s : List (X × ℕ)) (x : X) :
+    noise h (u :: s) x = (if u.1 ≠ x ∧ h u.1 = h x then u.2 else 0) + noise h s x := by
+  simp [noise]
+
+@[simp] theorem mass_append (s t : List (X × ℕ)) : mass (s ++ t) = mass s + mass t := by
+  simp [mass]
+
+@[simp] theorem frequency_append [DecidableEq X] (s t : List (X × ℕ)) (x : X) :
+    frequency (s ++ t) x = frequency s x + frequency t x := by
+  simp [frequency]
+
+@[simp] theorem bucket_append (h : X → Fin w) (s t : List (X × ℕ)) (b : Fin w) :
+    bucket h (s ++ t) b = bucket h s b + bucket h t b := by
+  simp [bucket]
+
+@[simp] theorem noise_append [DecidableEq X] (h : X → Fin w) (s t : List (X × ℕ)) (x : X) :
+    noise h (s ++ t) x = noise h s x + noise h t x := by
+  simp [noise]
+
+/-- A queried bucket consists of the query's frequency and nonnegative collision noise. -/
+theorem bucket_hash_eq_frequency_add_noise [DecidableEq X] (h : X → Fin w)
+    (s : List (X × ℕ)) (x : X) : bucket h s (h x) = frequency s x + noise h s x := by
+  induction s with
+  | nil => simp
+  | cons u s ih =>
+    by_cases hx : u.1 = x
+    · simp [hx, ih, Nat.add_assoc]
+    · by_cases hh : h u.1 = h x <;> simp [hx, hh, ih, Nat.add_left_comm]
+
+/-- A frequency cannot exceed the total inserted weight. -/
+theorem frequency_le_mass [DecidableEq X] (s : List (X × ℕ)) (x : X) :
+    frequency s x ≤ mass s := by
+  induction s with
+  | nil => simp
+  | cons u s ih =>
+    simp only [frequency_cons, mass_cons]
+    split_ifs <;> omega
+
+/-- Every bucket is bounded by the total inserted weight. -/
+theorem bucket_le_mass (h : X → Fin w) (s : List (X × ℕ)) (b : Fin w) :
+    bucket h s b ≤ mass s := by
+  induction s with
+  | nil => simp
+  | cons u s ih =>
+    simp only [bucket_cons, mass_cons]
+    split_ifs <;> omega
+
+/-- Collision noise is bounded by the total inserted weight. -/
+theorem noise_le_mass [DecidableEq X] (h : X → Fin w) (s : List (X × ℕ)) (x : X) :
+    noise h s x ≤ mass s :=
+  (Nat.le_add_left _ _).trans ((bucket_hash_eq_frequency_add_noise h s x) ▸
+    bucket_le_mass h s (h x))
+
+/-- A stored array of `d` rows of `w` natural-number counters. -/
+abbrev Table (d w : ℕ) := Vector (Vector ℕ w) d
+
+/-- The initial table has every counter zero. -/
+def zero (d w : ℕ) : Table d w := Vector.replicate d (Vector.replicate w 0)
+
+/-- Read one stored counter. -/
+def get (t : Table d w) (r : Fin d) (b : Fin w) : ℕ := t[r.val][b.val]
+
+/-- Add the update weight to the addressed counter in every row. -/
+def update (h : Fin d → X → Fin w) (t : Table d w) (u : X × ℕ) : Table d w :=
+  Vector.ofFn fun r => (t[r.val]).set (h r u.1).val (get t r (h r u.1) + u.2)
+
+/-- Process the stream in order, keeping only the current counter table. -/
+def run (h : Fin d → X → Fin w) (s : List (X × ℕ)) : Table d w :=
+  s.foldl (update h) (zero d w)
+
+/-- Merge tables formed with the same hash bank by adding corresponding counters. -/
+def merge (a b : Table d w) : Table d w :=
+  Vector.ofFn fun r => Vector.ofFn fun c => get a r c + get b r c
+
+/-- Take the minimum of the counters addressed by a query, using at least one row. -/
+def estimate [NeZero d] (h : Fin d → X → Fin w) (t : Table d w) (x : X) : ℕ :=
+  Finset.univ.inf' Finset.univ_nonempty fun r => get t r (h r x)
+
+@[simp] theorem get_zero (r : Fin d) (b : Fin w) : get (zero d w) r b = 0 := by
+  simp [get, zero]
+
+@[simp] theorem get_merge (a c : Table d w) (r : Fin d) (b : Fin w) :
+    get (merge a c) r b = get a r b + get c r b := by
+  simp [get, merge]
+
+/-- An update changes just its addressed bucket in each row. -/
+theorem get_update (h : Fin d → X → Fin w) (t : Table d w) (u : X × ℕ)
+    (r : Fin d) (b : Fin w) :
+    get (update h t u) r b = get t r b + if h r u.1 = b then u.2 else 0 := by
+  simp only [get, update, Vector.getElem_ofFn, Vector.getElem_set]
+  by_cases hb : h r u.1 = b
+  · simp [hb]
+  · have hv : (h r u.1).val ≠ b.val := fun hval => hb (Fin.ext hval)
+    simp [hb, hv]
+
+/-- An arbitrary starting table gains exactly the stream's bucket weights. -/
+theorem foldl_update_get (h : Fin d → X → Fin w) (s : List (X × ℕ))
+    (t : Table d w) (r : Fin d) (b : Fin w) :
+    get (s.foldl (update h) t) r b = get t r b + bucket (h r) s b := by
+  induction s generalizing t with
+  | nil => simp
+  | cons u s ih =>
+    rw [List.foldl_cons, ih, get_update, bucket_cons, Nat.add_assoc]
+
+/-- Every stored counter equals its exact weighted bucket sum. -/
+theorem run_get (h : Fin d → X → Fin w) (s : List (X × ℕ)) (r : Fin d) (b : Fin w) :
+    get (run h s) r b = bucket (h r) s b := by
+  rw [run, foldl_update_get, get_zero, Nat.zero_add]
+
+/-- Stored counters never exceed the total stream weight. -/
+theorem run_get_le_mass (h : Fin d → X → Fin w) (s : List (X × ℕ))
+    (r : Fin d) (b : Fin w) : get (run h s) r b ≤ mass s := by
+  rw [run_get]
+  exact bucket_le_mass (h r) s b
+
+/-- A query is no larger than any of its addressed row counters. -/
+theorem estimate_le_get [NeZero d] (h : Fin d → X → Fin w) (t : Table d w)
+    (x : X) (r : Fin d) : estimate h t x ≤ get t r (h r x) :=
+  Finset.inf'_le _ (Finset.mem_univ r)
+
+/-- A query on a processed stream is bounded by the exact bucket sum in every row. -/
+theorem estimate_run_le_bucket [NeZero d] (h : Fin d → X → Fin w) (s : List (X × ℕ))
+    (x : X) (r : Fin d) : estimate h (run h s) x ≤ bucket (h r) s (h r x) := by
+  rw [← run_get h s r (h r x)]
+  exact estimate_le_get h (run h s) x r
+
+/-- A Count-Min point query never underestimates the inserted frequency. -/
+theorem frequency_le_estimate_run [DecidableEq X] [NeZero d] (h : Fin d → X → Fin w)
+    (s : List (X × ℕ)) (x : X) : frequency s x ≤ estimate h (run h s) x := by
+  apply Finset.le_inf'
+  intro r _
+  rw [run_get, bucket_hash_eq_frequency_add_noise]
+  exact Nat.le_add_right _ _
+
+/-- Concatenating streams agrees exactly with merging tables using the same hash bank. -/
+theorem run_append (h : Fin d → X → Fin w) (s t : List (X × ℕ)) :
+    run h (s ++ t) = merge (run h s) (run h t) := by
+  apply Vector.ext
+  intro r hr
+  apply Vector.ext
+  intro b hb
+  change get (run h (s ++ t)) ⟨r, hr⟩ ⟨b, hb⟩ =
+    get (merge (run h s) (run h t)) ⟨r, hr⟩ ⟨b, hb⟩
+  rw [get_merge, run_get, run_get, run_get, bucket_append]
+
+/-- Appending one update performs one update on the current table. -/
+theorem run_append_singleton (h : Fin d → X → Fin w) (s : List (X × ℕ)) (u : X × ℕ) :
+    run h (s ++ [u]) = update h (run h s) u := by
+  simp [run, List.foldl_append]
+
+end Cslib.CountMin
diff --git a/Complexity/Algorithms/Streaming/CountMin/LinearHash.lean b/Complexity/Algorithms/Streaming/CountMin/LinearHash.lean
new file mode 100644
index 000000000..4e730ce64
--- /dev/null
+++ b/Complexity/Algorithms/Streaming/CountMin/LinearHash.lean
@@ -0,0 +1,72 @@
+/-
+Copyright (c) 2026 Samuel Schlesinger. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Samuel Schlesinger
+-/
+
+module
+-- upstream: candidate
+
+public import Complexity.Foundations.Data.BitString.Basic
+public import Complexity.Probability.BitString.LinearHash
+
+/-!
+# Binary-matrix hashes for Count-Min tables
+
+The existing binary linear hash family sends an `n`-bit item to `m` bits. Numbering that output
+with `BitString.equivFin m` gives a concrete universal family into `Fin (2 ^ m)`, suitable for
+the stored counters of a Count-Min table. The numbering is injective, so it does not change any
+collision event or require a stronger randomness assumption.
+
+A row seed consists of `m * n` bits. Sampling a tuple of these seeds uniformly gives the
+independent row seeds used by the Count-Min accuracy theorem. The seed-size statement below
+counts the seed space; hash evaluation and machine running times are separate obligations.
+
+## Main definitions
+
+* `Cslib.CountMin.indexedHash`: binary linear hashing with a finite bucket index as output.
+
+## Main results
+
+* `Cslib.CountMin.isTwoUniversal_indexedHash`: the concrete family is universal.
+* `Cslib.CountMin.card_indexedHash_seed`: a row has `2 ^ (m * n)` possible seeds.
+
+## References
+
+* [G. Cormode, S. Muthukrishnan, *An Improved Data Stream Summary: The Count-Min Sketch and its
+  Applications*, Sections 3 and 4.1][CormodeMuthukrishnan2005]
+* [I. Haitner, S. Vadhan, *The Many Entropies in One-Way Functions*][HaitnerVadhan2017],
+  Section 2.4.1, the Boolean-matrix example following Definition 4.
+-/
+
+@[expose] public section
+
+namespace Cslib.CountMin
+
+open Probability
+
+/-- Hash an `n`-bit item to one of `2 ^ m` numbered buckets using a binary `m × n` matrix. -/
+def indexedHash {n m : ℕ} (rows : Fin m → BitString n) (input : BitString n) : Fin (2 ^ m) :=
+  BitString.equivFin m (BitString.LinearHash.hash rows input)
+
+/-- Numbering the output bits leaves every collision event unchanged. -/
+@[simp] theorem indexedHash_eq_iff {n m : ℕ} (rows : Fin m → BitString n)
+    (x y : BitString n) :
+    indexedHash rows x = indexedHash rows y ↔
+      BitString.LinearHash.hash rows x = BitString.LinearHash.hash rows y :=
+  (BitString.equivFin m).injective.eq_iff
+
+/-- Uniform binary matrices give a universal family of Count-Min bucket indices. -/
+theorem isTwoUniversal_indexedHash (n m : ℕ) :
+    IsTwoUniversal (PMF.uniformOfFintype (Fin m → BitString n))
+      (indexedHash (n := n) (m := m)) := by
+  intro x y hxy
+  simpa only [indexedHash_eq_iff, Fintype.card_fin, BitString.card] using
+    BitString.LinearHash.isTwoUniversal n m x y hxy
+
+/-- A binary-matrix row seed has `m * n` Boolean coordinates. -/
+theorem card_indexedHash_seed (n m : ℕ) :
+    Fintype.card (Fin m → BitString n) = 2 ^ (m * n) := by
+  rw [Fintype.card_fun, BitString.card, Fintype.card_fin, ← pow_mul, Nat.mul_comm]
+
+end Cslib.CountMin
diff --git a/Complexity/Algorithms/Streaming/CountMin/Probability.lean b/Complexity/Algorithms/Streaming/CountMin/Probability.lean
new file mode 100644
index 000000000..8a52bcdc6
--- /dev/null
+++ b/Complexity/Algorithms/Streaming/CountMin/Probability.lean
@@ -0,0 +1,180 @@
+/-
+Copyright (c) 2026 Samuel Schlesinger. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Samuel Schlesinger
+-/
+
+module
+-- upstream: candidate
+
+public import Complexity.Algorithms.Streaming.CountMin.Basic
+public import Complexity.Probability.UniversalHash
+import Complexity.Foundations.Data.Finset.Expect
+import Complexity.Foundations.Data.Finset.Sampling
+import Mathlib.Tactic.FieldSimp
+import Mathlib.Tactic.Linarith
+import Mathlib.Tactic.Positivity
+
+/-!
+# Count-Min fixed-query accuracy
+
+For a fixed insertion-only weighted stream and a fixed queried item, independently sampled
+universal-hash rows give Count-Min its one-sided additive-error guarantee
+[CormodeMuthukrishnan2005], Section 4.1, Theorem 1. The stream and query are fixed before the
+hash seeds are sampled. This theorem makes no claim about adaptively selected queries or updates.
+
+The collision noise in one row has mean at most total stream mass divided by the bucket count.
+Markov's inequality bounds one bad row; independent uniform row seeds raise its failure bound
+to the number of rows. In particular, `2 ≤ w * ε` gives failure at most `2⁻ᵈ`.
+
+## Main results
+
+* `Cslib.CountMin.expect_noise_le`: expected single-row collision noise.
+* `Cslib.CountMin.dens_noise_gt_le`: single-row tail bound.
+* `Cslib.CountMin.dens_estimate_gt_le`: independent-row amplification at an absolute threshold.
+* `Cslib.CountMin.dens_estimate_error_le`: relative additive error for a fixed query.
+* `Cslib.CountMin.dens_estimate_error_le_inv_two_pow`: the base-two parameter guarantee.
+
+## References
+
+* [G. Cormode, S. Muthukrishnan, *An Improved Data Stream Summary: The Count-Min Sketch
+  and its Applications*][CormodeMuthukrishnan2005], Section 4.1, Theorem 1.
+-/
+
+@[expose] public section
+
+namespace Cslib.CountMin
+
+open Finset Probability
+open scoped BigOperators
+
+variable {X Seed : Type*} [DecidableEq X] [Fintype Seed] [Nonempty Seed] {d w : ℕ}
+
+/-- The expected collision noise of one universal-hash row is at most total mass divided by
+the number of buckets. No finiteness assumption on the item universe is needed. -/
+theorem expect_noise_le (hash : Seed → X → Fin w)
+    (hh : IsTwoUniversal (PMF.uniformOfFintype Seed) hash) (s : List (X × ℕ)) (x : X) :
+    (𝔼 seed, (noise (hash seed) s x : ℝ)) ≤ (mass s : ℝ) / w := by
+  induction s with
+  | nil => simp [noise, mass]
+  | cons event s ih =>
+    rcases event with ⟨y, c⟩
+    simp only [noise_cons, mass_cons, Nat.cast_add, expect_add_distrib, add_div]
+    refine add_le_add ?_ ih
+    by_cases hy : y = x
+    · simp only [hy, ne_eq, not_true_eq_false, false_and, ite_false, Nat.cast_zero,
+        Fintype.expect_const]
+      positivity
+    · have hcoll := hh.expect_boole_le hy
+      simp only [Fintype.card_fin] at hcoll
+      calc
+        (𝔼 seed, ((if y ≠ x ∧ hash seed y = hash seed x then c else 0 : ℕ) : ℝ)) =
+            (c : ℝ) * (𝔼 seed, if hash seed y = hash seed x then (1 : ℝ) else 0) := by
+          rw [mul_expect]
+          apply expect_congr rfl
+          intro seed _
+          simp [hy]
+        _ ≤ (c : ℝ) * (w : ℝ)⁻¹ := mul_le_mul_of_nonneg_left hcoll (Nat.cast_nonneg c)
+        _ = (c : ℝ) / w := (div_eq_mul_inv _ _).symm
+
+/-- Markov's inequality bounds the fraction of seeds whose collision noise exceeds `t`. -/
+theorem dens_noise_gt_le (hash : Seed → X → Fin w)
+    (hh : IsTwoUniversal (PMF.uniformOfFintype Seed) hash) (s : List (X × ℕ)) (x : X)
+    {t : ℝ} (ht : 0 < t) :
+    (dens {seed | t < (noise (hash seed) s x : ℝ)} : ℝ) ≤ (mass s : ℝ) / (w * t) := by
+  classical
+  have hsub :
+      (dens {seed | t < (noise (hash seed) s x : ℝ)} : ℝ) ≤
+        dens {seed | t ≤ (noise (hash seed) s x : ℝ)} := by
+    exact_mod_cast dens_mono (fun seed hseed => by
+      simp only [mem_filter, mem_univ, true_and] at hseed ⊢
+      exact hseed.le)
+  have hmarkov := Fintype.mul_dens_filter_le_expect
+    (f := fun seed => (noise (hash seed) s x : ℝ)) (fun _ => Nat.cast_nonneg _) t
+  have hbound := (mul_le_mul_of_nonneg_left hsub ht.le).trans
+    (hmarkov.trans (expect_noise_le hash hh s x))
+  calc
+    _ ≤ ((mass s : ℝ) / w) / t :=
+      (le_div_iff₀ ht).mpr (by simpa only [mul_comm] using hbound)
+    _ = _ := div_div _ _ _
+
+/-- Count-Min can exceed a fixed absolute additive threshold only when every independent
+row exceeds that threshold. -/
+theorem dens_estimate_gt_le [NeZero d] (hash : Seed → X → Fin w)
+    (hh : IsTwoUniversal (PMF.uniformOfFintype Seed) hash) (s : List (X × ℕ)) (x : X)
+    {t : ℝ} (ht : 0 < t) :
+    (dens {seeds : Fin d → Seed |
+      (frequency s x : ℝ) + t <
+        (estimate (fun r => hash (seeds r)) (run (fun r => hash (seeds r)) s) x : ℝ)} : ℝ) ≤
+      ((mass s : ℝ) / (w * t)) ^ d := by
+  classical
+  let bad : Finset Seed := {seed | t < (noise (hash seed) s x : ℝ)}
+  have hsub :
+      ({seeds : Fin d → Seed | (frequency s x : ℝ) + t <
+        (estimate (fun r => hash (seeds r)) (run (fun r => hash (seeds r)) s) x : ℝ)} :
+          Finset (Fin d → Seed)) ⊆
+      Fintype.piFinset (fun _ : Fin d => bad) := by
+    intro seeds hseeds
+    simp only [mem_filter, mem_univ, true_and] at hseeds
+    apply Fintype.mem_piFinset.mpr
+    intro r
+    simp only [bad, mem_filter, mem_univ, true_and]
+    have hrow :
+        (estimate (fun r => hash (seeds r)) (run (fun r => hash (seeds r)) s) x : ℝ) ≤
+          (bucket (hash (seeds r)) s (hash (seeds r) x) : ℝ) := by
+      exact_mod_cast estimate_run_le_bucket (fun r => hash (seeds r)) s x r
+    rw [bucket_hash_eq_frequency_add_noise, Nat.cast_add] at hrow
+    linarith
+  calc
+    _ ≤ (dens (Fintype.piFinset (fun _ : Fin d => bad)) : ℝ) := by
+      exact_mod_cast dens_mono hsub
+    _ = (dens bad : ℝ) ^ d := by
+      rw [Fintype.dens_piFinset_const, Fintype.card_fin, NNRat.cast_pow]
+    _ ≤ _ := pow_le_pow_left₀ (NNRat.cast_nonneg _)
+      (dens_noise_gt_le hash hh s x ht) d
+
+/-- A fixed Count-Min query has additive error at most `ε * mass s` except on a fraction
+`(w * ε)⁻ᵈ` of the independently sampled uniform hash banks. -/
+theorem dens_estimate_error_le [NeZero d] [NeZero w] (hash : Seed → X → Fin w)
+    (hh : IsTwoUniversal (PMF.uniformOfFintype Seed) hash) (s : List (X × ℕ)) (x : X)
+    {ε : ℝ} (hε : 0 < ε) :
+    (dens {seeds : Fin d → Seed |
+      (frequency s x : ℝ) + ε * mass s <
+        (estimate (fun r => hash (seeds r)) (run (fun r => hash (seeds r)) s) x : ℝ)} : ℝ) ≤
+      ((w : ℝ) * ε)⁻¹ ^ d := by
+  classical
+  by_cases hm : mass s = 0
+  · have hempty :
+        ({seeds : Fin d → Seed | (frequency s x : ℝ) + ε * mass s <
+          (estimate (fun r => hash (seeds r)) (run (fun r => hash (seeds r)) s) x : ℝ)} :
+            Finset (Fin d → Seed)) = ∅ := by
+      apply eq_empty_of_forall_notMem
+      intro seeds hseeds
+      simp only [mem_filter, mem_univ, true_and, hm, Nat.cast_zero, mul_zero, add_zero] at hseeds
+      have hrow := estimate_run_le_bucket (fun r => hash (seeds r)) s x (0 : Fin d)
+      have hmass := bucket_le_mass (hash (seeds 0)) s (hash (seeds 0) x)
+      have hz : estimate (fun r => hash (seeds r))
+          (run (fun r => hash (seeds r)) s) x = 0 := Nat.eq_zero_of_le_zero (hm ▸ hrow.trans hmass)
+      rw [hz, Nat.cast_zero] at hseeds
+      exact (not_lt_of_ge (Nat.cast_nonneg _)) hseeds
+    rw [hempty, dens_empty, NNRat.cast_zero]
+    positivity
+  · have hmpos : (0 : ℝ) < mass s := by exact_mod_cast Nat.pos_of_ne_zero hm
+    have hwpos : (0 : ℝ) < w := by exact_mod_cast Nat.pos_of_ne_zero (NeZero.ne w)
+    have heq : (mass s : ℝ) / (w * (ε * mass s)) = ((w : ℝ) * ε)⁻¹ := by
+      field_simp
+    simpa only [heq] using dens_estimate_gt_le (d := d) hash hh s x (mul_pos hε hmpos)
+
+/-- With at least `2 / ε` buckets, each additional independent row halves the failure bound. -/
+theorem dens_estimate_error_le_inv_two_pow [NeZero d] [NeZero w]
+    (hash : Seed → X → Fin w) (hh : IsTwoUniversal (PMF.uniformOfFintype Seed) hash)
+    (s : List (X × ℕ)) (x : X) {ε : ℝ} (hε : 0 < ε) (hw : 2 ≤ (w : ℝ) * ε) :
+    (dens {seeds : Fin d → Seed |
+      (frequency s x : ℝ) + ε * mass s <
+        (estimate (fun r => hash (seeds r)) (run (fun r => hash (seeds r)) s) x : ℝ)} : ℝ) ≤
+      (2 ^ d : ℝ)⁻¹ := by
+  refine (dens_estimate_error_le hash hh s x hε).trans ?_
+  rw [← inv_pow]
+  exact pow_le_pow_left₀ (by positivity) (inv_anti₀ (by norm_num) hw) d
+
+end Cslib.CountMin
diff --git a/Complexity/Algorithms/Streaming/CountMin/Program.lean b/Complexity/Algorithms/Streaming/CountMin/Program.lean
new file mode 100644
index 000000000..29d4cec71
--- /dev/null
+++ b/Complexity/Algorithms/Streaming/CountMin/Program.lean
@@ -0,0 +1,133 @@
+/-
+Copyright (c) 2026 Samuel Schlesinger. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Samuel Schlesinger
+-/
+
+module
+-- upstream: candidate
+
+public import Complexity.Algorithms.Streaming.CountMin.Probability
+public import Complexity.Languages.Probabilistic.Vector
+import Complexity.Probability.PMF.Uniform
+
+/-!
+# Count-Min as a probabilistic program
+
+`sampleSketch` independently repeats a caller-supplied seed sampler and processes a weighted
+insertion stream with the resulting hash rows. Its output retains both the row seeds and the
+materialized counter table, so later queries use the same hashes. `sampleQuery` constructs a
+sketch and returns one point query. The hash family is supplied separately and must remain fixed
+between construction and queries.
+
+When one seed is exactly uniform, repeated calls give the uniform distribution on row-seed
+tuples. This identifies the output law of the program with the deterministic construction
+analyzed in `CountMin.Probability`, giving its fixed-query failure bound. The stream and query
+are fixed before the seeds are sampled. No running-time or representation cost is asserted for
+the supplied sampler, hash function, or program.
+
+## Main definitions
+
+* `Cslib.CountMin.Sketch`: row seeds together with the stored counter table.
+* `Cslib.CountMin.buildSketch`, `Cslib.CountMin.Sketch.query`: deterministic construction and
+  point queries retaining the construction's hashes.
+* `Cslib.CountMin.sampleSketch`, `Cslib.CountMin.sampleQuery`: probabilistic construction and
+  a fixed point query.
+
+## Main results
+
+* `Cslib.CountMin.eval_sampleSketch`, `Cslib.CountMin.eval_sampleQuery`: output laws under a
+  uniform seed sampler.
+* `Cslib.CountMin.frequency_le_of_mem_support_sampleQuery`: every possible query result avoids
+  underestimation, without any uniformity assumption.
+* `Cslib.CountMin.sampleQuery_error_le_inv_two_pow`: failure probability at most `2⁻ᵈ` when
+  `2 ≤ w * ε`, for a two-universal hash family and a uniform seed sampler.
+
+## References
+
+* [G. Cormode, S. Muthukrishnan, *An Improved Data Stream Summary: The Count-Min Sketch
+  and its Applications*][CormodeMuthukrishnan2005], Section 4.1, Theorem 1.
+-/
+
+@[expose] public section
+
+namespace Cslib.CountMin
+
+open Probability
+
+variable {X : Type*} {Seed : Type} {d w : ℕ}
+
+/-- A stored sketch retains its sampled row seeds and materialized counter table. -/
+structure Sketch (Seed : Type) (d w : ℕ) where
+  /-- One seed for each hash row. -/
+  seeds : Fin d → Seed
+  /-- The counters updated using these row seeds. -/
+  table : Table d w
+
+/-- Process a stream with a fixed row-seed tuple, retaining it for later queries. -/
+def buildSketch (hash : Seed → X → Fin w) (s : List (X × ℕ))
+    (seeds : Fin d → Seed) : Sketch Seed d w :=
+  ⟨seeds, run (fun r => hash (seeds r)) s⟩
+
+/-- Query the stored table using the same hash family as in its construction. -/
+def Sketch.query [NeZero d] (sketch : Sketch Seed d w) (hash : Seed → X → Fin w)
+    (x : X) : ℕ :=
+  estimate (fun r => hash (sketch.seeds r)) sketch.table x
+
+/-- Draw independent row seeds and build the stored sketch for the supplied stream. -/
+def sampleSketch (sampleSeed : ProbComp Seed) (hash : Seed → X → Fin w)
+    (s : List (X × ℕ)) : ProbComp (Sketch Seed d w) :=
+  buildSketch hash s <$> OracleComp.replicateFin d sampleSeed
+
+/-- Build a sketch and return its estimate for one fixed point query. -/
+def sampleQuery [NeZero d] (sampleSeed : ProbComp Seed) (hash : Seed → X → Fin w)
+    (s : List (X × ℕ)) (x : X) : ProbComp ℕ :=
+  (fun sketch => sketch.query hash x) <$> sampleSketch (d := d) sampleSeed hash s
+
+/-- A uniform seed sampler gives the deterministic construction a uniform row-seed tuple. -/
+theorem eval_sampleSketch [Fintype Seed] [Nonempty Seed] (sampleSeed : ProbComp Seed)
+    (hs : ProbComp.eval sampleSeed = PMF.uniformOfFintype Seed)
+    (hash : Seed → X → Fin w) (s : List (X × ℕ)) :
+    ProbComp.eval (sampleSketch (d := d) sampleSeed hash s) =
+      (PMF.uniformOfFintype (Fin d → Seed)).map (buildSketch hash s) := by
+  simp only [sampleSketch, ProbComp.eval_map, ProbComp.eval_replicateFin, hs,
+    PMF.pi_uniformOfFintype]
+
+/-- The point-query program has the law of querying a uniformly sampled hash bank. -/
+theorem eval_sampleQuery [Fintype Seed] [Nonempty Seed] [NeZero d]
+    (sampleSeed : ProbComp Seed) (hs : ProbComp.eval sampleSeed = PMF.uniformOfFintype Seed)
+    (hash : Seed → X → Fin w) (s : List (X × ℕ)) (x : X) :
+    ProbComp.eval (sampleQuery (d := d) sampleSeed hash s x) =
+      (PMF.uniformOfFintype (Fin d → Seed)).map (fun seeds =>
+        estimate (fun r => hash (seeds r)) (run (fun r => hash (seeds r)) s) x) := by
+  rw [sampleQuery, ProbComp.eval_map, eval_sampleSketch sampleSeed hs, PMF.map_comp]
+  rfl
+
+/-- Every possible output of the point-query program is at least the true frequency. -/
+theorem frequency_le_of_mem_support_sampleQuery [DecidableEq X] [NeZero d]
+    (sampleSeed : ProbComp Seed) (hash : Seed → X → Fin w) (s : List (X × ℕ)) (x : X)
+    {answer : ℕ} (ha : answer ∈ (ProbComp.eval
+      (sampleQuery (d := d) sampleSeed hash s x)).support) : frequency s x ≤ answer := by
+  rw [sampleQuery, ProbComp.eval_map, PMF.mem_support_map_iff] at ha
+  rcases ha with ⟨sketch, hsketch, rfl⟩
+  rw [sampleSketch, ProbComp.eval_map, PMF.mem_support_map_iff] at hsketch
+  rcases hsketch with ⟨seeds, _, rfl⟩
+  exact frequency_le_estimate_run (fun r => hash (seeds r)) s x
+
+/-- The actual point-query program has failure probability at most `2⁻ᵈ` with at least
+`2 / ε` buckets and independently uniform seeds for a two-universal hash family. -/
+theorem sampleQuery_error_le_inv_two_pow [DecidableEq X] [Fintype Seed] [Nonempty Seed]
+    [NeZero d] [NeZero w] (sampleSeed : ProbComp Seed)
+    (hs : ProbComp.eval sampleSeed = PMF.uniformOfFintype Seed)
+    (hash : Seed → X → Fin w) (hh : IsTwoUniversal (PMF.uniformOfFintype Seed) hash)
+    (s : List (X × ℕ)) (x : X) {ε : ℝ} (hε : 0 < ε) (hw : 2 ≤ (w : ℝ) * ε) :
+    ((ProbComp.eval (sampleQuery (d := d) sampleSeed hash s x)).toOuterMeasure
+      {answer | (frequency s x : ℝ) + ε * mass s < (answer : ℝ)}).toReal ≤
+        (2 ^ d : ℝ)⁻¹ := by
+  classical
+  rw [eval_sampleQuery sampleSeed hs, PMF.toOuterMeasure_map_apply,
+    PMF.toOuterMeasure_uniformOfFintype_toReal]
+  simpa only [Finset.nnratCast_dens, Set.mem_preimage, Set.mem_ofPred_eq] using
+    dens_estimate_error_le_inv_two_pow (d := d) hash hh s x hε hw
+
+end Cslib.CountMin
diff --git a/Complexity/Foundations/Data/Finset/Sampling.lean b/Complexity/Foundations/Data/Finset/Sampling.lean
index f16203c43..d9c1ab29a 100644
--- a/Complexity/Foundations/Data/Finset/Sampling.lean
+++ b/Complexity/Foundations/Data/Finset/Sampling.lean
@@ -115,7 +115,8 @@ section RepeatedTrials
 
 variable [DecidableEq ι]
 
-private theorem dens_piFinset_const (t : Finset α) :
+/-- Independent uniform coordinates all belong to `t` with probability `dens t ^ card ι`. -/
+theorem dens_piFinset_const (t : Finset α) :
     dens (piFinset fun _ : ι => t) = dens t ^ card ι := by
   rw [dens_eq_card_div_card, card_piFinset, prod_const, card_univ, card_fun,
     dens_eq_card_div_card]
diff --git a/ComplexityTests/CountMin.lean b/ComplexityTests/CountMin.lean
new file mode 100644
index 000000000..36fe38041
--- /dev/null
+++ b/ComplexityTests/CountMin.lean
@@ -0,0 +1,103 @@
+/-
+Copyright (c) 2026 Samuel Schlesinger. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Samuel Schlesinger
+-/
+
+module
+
+public import Complexity.Algorithms.Streaming.CountMin.LinearHash
+public import Complexity.Algorithms.Streaming.CountMin.Program
+import Mathlib.Tactic.NormNum
+
+/-! # Count-Min clients
+
+The executable examples check stored rows, weighted updates, an absent queried item, and merging.
+The probabilistic example instantiates the proved bound with an existing concrete universal hash
+family, four buckets and three independent rows.
+-/
+
+public section
+
+namespace ComplexityTests.CountMin
+
+open Cslib Cslib.CountMin Cslib.Probability
+
+/-- Two rows distinguishing the low and high bits of a two-bit item. -/
+private def hashBank (r : Fin 2) (x : Fin 4) : Fin 2 :=
+  if r = 0 then ⟨x.val % 2, Nat.mod_lt _ (by decide)⟩
+  else ⟨x.val / 2, by omega⟩
+
+/-- Three distinct items with unequal positive weights; item `3` never occurs. -/
+private def stream : List (Fin 4 × ℕ) := [(0, 2), (1, 3), (2, 5)]
+
+-- This checks the actual nested-vector representation, including collisions in both rows.
+example : ((run hashBank stream).toList.map Vector.toList) = [[7, 3], [5, 5]] := by
+  decide
+
+example : List.ofFn (fun x : Fin 4 => estimate hashBank (run hashBank stream) x) =
+    [5, 3, 5, 3] := by
+  decide
+
+-- An absent item can have a positive estimate; Count-Min's guarantee is one-sided.
+example : frequency stream 3 = 0 ∧ estimate hashBank (run hashBank stream) 3 = 3 := by
+  decide
+
+example (x : Fin 4) : frequency stream x ≤ estimate hashBank (run hashBank stream) x :=
+  frequency_le_estimate_run hashBank stream x
+
+-- A repeated item adds its entire weight to the two addressed counters.
+example : ((update hashBank (run hashBank stream) (0, 4)).toList.map Vector.toList) =
+    [[11, 3], [9, 5]] := by
+  decide
+
+example : merge (run hashBank [(0, 2)]) (run hashBank [(1, 3), (2, 5)]) =
+    run hashBank stream := by
+  decide
+
+example : ((run hashBank []).toList.map Vector.toList) = [[0, 0], [0, 0]] ∧
+    estimate hashBank (run hashBank []) 3 = 0 := by
+  decide
+
+-- Zero mass does not require the stream to be empty.
+example : mass ([(0, 0), (2, 0)] : List (Fin 4 × ℕ)) = 0 ∧
+    run hashBank [(0, 0), (2, 0)] = zero 2 2 ∧
+    ∀ x : Fin 4, estimate hashBank (run hashBank [(0, 0), (2, 0)]) x = 0 := by
+  decide
+
+/-- Four buckets and three independent matrix seeds give additive error at most half the mass,
+except on at most one eighth of the hash banks, for any fixed stream and query. -/
+theorem fixed_query_error_le_one_eighth {n : ℕ} (s : List (BitString n × ℕ)) (x : BitString n) :
+    (Finset.dens {seeds : Fin 3 → Fin 2 → BitString n |
+      (frequency s x : ℝ) + (1 / 2 : ℝ) * mass s <
+        (estimate (fun r => indexedHash (seeds r))
+          (run (fun r => indexedHash (seeds r)) s) x : ℝ)} : ℝ) ≤ 1 / 8 := by
+  convert dens_estimate_error_le_inv_two_pow (d := 3)
+    (indexedHash (n := n) (m := 2)) (isTwoUniversal_indexedHash n 2) s x
+    (ε := (1 / 2 : ℝ)) (by norm_num) (by norm_num) using 1
+  norm_num
+
+-- The same theorem accepts a nonempty stream of total weight zero.
+example {n : ℕ} (item x : BitString n) :
+    (Finset.dens {seeds : Fin 3 → Fin 2 → BitString n |
+      0 < (estimate (fun r => indexedHash (seeds r))
+        (run (fun r => indexedHash (seeds r)) [(item, 0)]) x : ℝ)} : ℝ) ≤ 1 / 8 := by
+  have h := dens_estimate_error_le_inv_two_pow (d := 3)
+    (indexedHash (n := n) (m := 2)) (isTwoUniversal_indexedHash n 2) [(item, 0)] x
+    (ε := (1 / 2 : ℝ)) (by norm_num) (by norm_num)
+  norm_num [frequency, mass] at h ⊢
+  exact h
+
+-- A concrete sampler satisfies the uniformity premise of the probabilistic-program theorem.
+example {n : ℕ} (s : List (BitString n × ℕ)) (x : BitString n) :
+    ((ProbComp.eval (sampleQuery (d := 3) (ProbComp.uniform (Fin 2 → BitString n))
+      (indexedHash (n := n) (m := 2)) s x)).toOuterMeasure
+        {answer | (frequency s x : ℝ) + (1 / 2 : ℝ) * mass s < (answer : ℝ)}).toReal ≤
+      1 / 8 := by
+  convert sampleQuery_error_le_inv_two_pow (d := 3)
+    (ProbComp.uniform (Fin 2 → BitString n)) (ProbComp.eval_uniform (Fin 2 → BitString n))
+    (indexedHash (n := n) (m := 2)) (isTwoUniversal_indexedHash n 2) s x
+    (ε := (1 / 2 : ℝ)) (by norm_num) (by norm_num) using 1
+  norm_num
+
+end ComplexityTests.CountMin
diff --git a/README.md b/README.md
index f1aa99e6c..8e7810667 100644
--- a/README.md
+++ b/README.md
@@ -22,6 +22,7 @@ mathematics. See [Contributing](CONTRIBUTING.md) to propose, implement, or revie
 | State P/NP membership or prove a problem NP-complete | [Checked plain examples](ComplexityTests/NPCompleteness.lean), then [Clique](Complexity/Computability/Complexity/Problems/Clique.lean) |
 | Construct circuits for polynomial-time function families | [Uniform circuit examples](ComplexityTests/UniformCircuits.lean) |
 | Write probabilistic programs or oracle reductions | [PPT examples](ComplexityTests/PPTTactic.lean), [oracle examples](ComplexityTests/OraclePPT.lean) |
+| Estimate frequencies in a stream | [Count-Min examples](ComplexityTests/CountMin.lean), then [fixed-query accuracy](Complexity/Algorithms/Streaming/CountMin/Probability.lean) |
 | Find a computational model or mathematical tool | [Search the API documentation](https://www.cslib.io/complexitylib/search.html), rebuilt nightly from `main`; [Complexity.lean](Complexity.lean) lists every module, and each documents its definitions, results, and references |
 | Contribute a result or improve an API | [Contributing](CONTRIBUTING.md) |
 
diff --git a/ROADMAP.md b/ROADMAP.md
index 114ce329e..715a426f1 100644
--- a/ROADMAP.md
+++ b/ROADMAP.md
@@ -339,6 +339,10 @@ each statement against the numbered result. Organize modules by subject, not cha
   separations, and randomized lifting.
 - Multiparty protocols, discrepancy and information complexity, direct-sum and direct-product
   results, and reductions to streaming, sketching and cell-probe lower bounds.
+- **Streaming and sketching:** native time and space bounds for Count-Min, including hash-seed
+  storage and evaluation; AMS frequency moments, CountSketch, turnstile updates, and heavy-hitter
+  recovery; communication-to-streaming transfers with explicit state encodings and pass counts.
+  The first Count-Min milestone is scoped in [#1201](https://github.com/cslib-community/complexitylib/issues/1201).
 - **Learning:** machine-certified running times for the LMN and Kushilevitz–Mansour learners;
   distributional problems and reductions, samplability, average-to-worst-case connections,
   PAC/agnostic/SQ learning, learning lower bounds, compression and refutation.
diff --git a/guide/ComplexityGuide.lean b/guide/ComplexityGuide.lean
index 57a8cef1f..c741152ae 100644
--- a/guide/ComplexityGuide.lean
+++ b/guide/ComplexityGuide.lean
@@ -6,6 +6,7 @@ Authors: Samuel Schlesinger
 import VersoManual
 import ComplexityGuide.FirstSteps
 import ComplexityGuide.NPCompleteness
+import ComplexityGuide.Streaming
 
 open Verso.Genre Manual
 
@@ -31,9 +32,9 @@ docstring and source. Other entry points:
 * [ROADMAP.md][roadmap] records outstanding work, and [CONTRIBUTING.md][contributing] explains how
   to propose and review changes.
 
-The guide is new: after first steps, it has a chapter on NP-completeness. Further areas follow
-one at a time, and each chapter's friction points are fixed in the library rather than documented
-around.
+The guide is new: after first steps, it has chapters on NP-completeness and streaming. Further
+areas follow one at a time, and each chapter's friction points are fixed in the library rather
+than documented around.
 
 [cslib]: https://github.com/leanprover/cslib
 [api]: https://www.cslib.io/complexitylib/
@@ -46,3 +47,5 @@ around.
 {include 1 ComplexityGuide.FirstSteps}
 
 {include 1 ComplexityGuide.NPCompleteness}
+
+{include 1 ComplexityGuide.Streaming}
diff --git a/guide/ComplexityGuide/Streaming.lean b/guide/ComplexityGuide/Streaming.lean
new file mode 100644
index 000000000..d58d8e8d5
--- /dev/null
+++ b/guide/ComplexityGuide/Streaming.lean
@@ -0,0 +1,140 @@
+/-
+Copyright (c) 2026 Samuel Schlesinger. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Samuel Schlesinger
+-/
+import VersoManual
+import Complexity.Algorithms.Streaming.CountMin.LinearHash
+import Complexity.Algorithms.Streaming.CountMin.Program
+
+open Verso.Genre Manual
+open Verso.Genre.Manual.InlineLean
+
+set_option pp.rawOnError true
+set_option verso.code.warnLineLength 80
+
+#doc (Manual) "Streaming and Sketching" =>
+%%%
+tag := "streaming-and-sketching"
+%%%
+
+A frequency sketch processes updates while keeping a table of counters. A query estimates how
+much weight an item has received. Count-Min provides a useful first example: its estimate is
+always at least the true frequency, and independently sampled hash rows bound the probability
+of a large overestimate.
+
+This chapter uses weighted insertions. An event `(x, c)` adds the natural number `c` to item `x`;
+the stream is a `List (X × ℕ)`. The list describes the input to the correctness theorem. The
+stored table contains only counters, and {name}`Cslib.CountMin.update` can process one new event
+from the current table.
+
+```
+import Complexity.Algorithms.Streaming.CountMin.LinearHash
+import Complexity.Algorithms.Streaming.CountMin.Program
+
+open Cslib.CountMin
+```
+
+```lean -show
+open Cslib.CountMin
+```
+
+# Updates and Queries
+%%%
+tag := "count-min-updates"
+%%%
+
+{name}`Cslib.CountMin.Table` `d w` is a vector of `d` rows, each with `w` natural-number counters.
+A hash bank `h : Fin d → X → Fin w` selects one bucket per row for each item. An update adds its
+weight to those buckets. {name}`Cslib.CountMin.run` folds the update function over the stream,
+starting from zero. A query takes the minimum of its addressed counters, so queries require
+at least one row.
+
+Here two rows hash the low and high bits of four possible items. Item `3` is absent from the
+stream, and the other three items have different weights.
+
+```lean
+def exampleHash (r : Fin 2) (x : Fin 4) : Fin 2 :=
+  if r = 0 then ⟨x.val % 2, Nat.mod_lt _ (by decide)⟩
+  else ⟨x.val / 2, by omega⟩
+
+def exampleStream : List (Fin 4 × ℕ) := [(0, 2), (1, 3), (2, 5)]
+
+example : (run exampleHash exampleStream).toList.map Vector.toList =
+    [[7, 3], [5, 5]] := by
+  decide
+
+example : List.ofFn (fun x : Fin 4 =>
+    estimate exampleHash (run exampleHash exampleStream) x) =
+      [5, 3, 5, 3] := by
+  decide
+```
+
+The true frequencies are `2, 3, 5, 0`. Collisions increase the estimates for items `0` and `3`.
+An absent item can therefore have a positive estimate. The deterministic guarantee is
+{name}`Cslib.CountMin.frequency_le_estimate_run`:
+
+```lean
+example (x : Fin 4) : frequency exampleStream x ≤
+    estimate exampleHash (run exampleHash exampleStream) x :=
+  frequency_le_estimate_run exampleHash exampleStream x
+```
+
+# Merging Streams
+%%%
+tag := "count-min-merging"
+%%%
+
+Tables computed with the same hash bank merge by adding corresponding counters.
+{name}`Cslib.CountMin.run_append` identifies this operation with processing the concatenated
+streams. The equality concerns the whole table; taking minima does not make point estimates
+additive.
+
+```lean
+example : merge (run exampleHash [(0, 2)])
+    (run exampleHash [(1, 3), (2, 5)]) = run exampleHash exampleStream := by
+  decide
+```
+
+For online processing, {name}`Cslib.CountMin.run_append_singleton` identifies appending one
+event to the input with applying one update to the current table.
+
+# Randomness and Accuracy
+%%%
+tag := "count-min-accuracy"
+%%%
+
+The random choice is a seed for each hash row. A two-universal family bounds the collision
+probability of any two distinct items by the reciprocal of the number of buckets. Count-Min
+needs independent row seeds as well: the guarantee samples a uniform tuple of seeds, rather
+than reusing one seed across all rows.
+
+For a stream and query fixed before sampling, let `M` be {name}`Cslib.CountMin.mass` of the
+stream and let `f` be the queried frequency. The theorem
+{name}`Cslib.CountMin.dens_estimate_error_le` bounds the probability that the estimate exceeds
+`f + ε * M` by `(w * ε)⁻¹ ^ d`, for positive `ε`, `w`, and `d`.
+{name}`Cslib.CountMin.dens_estimate_error_le_inv_two_pow` specializes this to `2⁻ᵈ` when
+`2 ≤ w * ε`. With four buckets, three rows, and `ε = 1/2`, the bound is `1/8`.
+Zero total weight is included and gives an identically zero table.
+
+The concrete family {name}`Cslib.CountMin.indexedHash` hashes `n`-bit items to `2^m` buckets
+using a binary matrix with `m` rows. Its collision guarantee is
+{name}`Cslib.CountMin.isTwoUniversal_indexedHash`. Each row of the sketch needs a separate
+matrix seed with `m * n` bits.
+
+{name}`Cslib.CountMin.sampleSketch` is a `ProbComp` program that calls a supplied seed sampler
+independently for each row, then processes the stream. Its result stores the seeds and counter
+table; later queries must use the same hash family. The evaluation theorem assumes that one
+call to the sampler is exactly uniform. {name}`Cslib.CountMin.sampleQuery` constructs a sketch
+and returns one fixed query, and {name}`Cslib.CountMin.sampleQuery_error_le_inv_two_pow`
+proves the same failure bound for the actual program's output law.
+
+These results formalize Count-Min's insertion-only point-query guarantee from
+[Cormode and Muthukrishnan, Section 4.1, Theorem 1][count-min]. They do not cover adaptive
+updates or queries, deletions, or heavy-hitter enumeration. The table has `d * w` counters,
+each at most `M`, but machine time and bit-space certificates, including the hash seeds, remain
+separate work. The [checked examples][examples] include concrete collisions, merging, zero
+weights, and a universal-hash accuracy instance.
+
+[count-min]: https://www.cs.ox.ac.uk/people/graham.cormode/pubs/papers/cm-full.pdf
+[examples]: https://github.com/cslib-community/complexitylib/blob/main/ComplexityTests/CountMin.lean
diff --git a/references.bib b/references.bib
index 6b32ca500..945d5311a 100644
--- a/references.bib
+++ b/references.bib
@@ -1052,6 +1052,18 @@ @article{CoppersmithRivlin1992
   doi       = {10.1137/0523054}
 }
 
+@article{CormodeMuthukrishnan2005,
+  author    = {Cormode, Graham and Muthukrishnan, S.},
+  title     = {An Improved Data Stream Summary: The {Count-Min} Sketch and its Applications},
+  journal   = {Journal of Algorithms},
+  volume    = {55},
+  number    = {1},
+  pages     = {58--75},
+  year      = {2005},
+  doi       = {10.1016/j.jalgor.2003.12.001},
+  url       = {https://www.cs.ox.ac.uk/people/graham.cormode/pubs/papers/cm-full.pdf}
+}
+
 @book{CoverThomas2006,
   author    = {Cover, Thomas M. and Thomas, Joy A.},
   title     = {Elements of Information Theory},