diff --git a/Complexity/Foundations/Probability/HeavyCount.lean b/Complexity/Foundations/Probability/HeavyCount.lean
index 7d54813038..1684783528 100644
--- a/Complexity/Foundations/Probability/HeavyCount.lean
+++ b/Complexity/Foundations/Probability/HeavyCount.lean
@@ -17,9 +17,11 @@ import Mathlib.Tactic.Ring
 /-!
 # Conditional rarity of retained heavy entries
 
-A row with first signal `d` has bounded mass `a * ∑ w, d w ≤ M`. At a floor `ρ > 0`,
-there are at most `4 * M / (a * ρ)` entries above `ρ / 4`. Suppose that, on a finite slice
-of draws, every endpoint other than one specified endpoint is retained on at most a
+A row on a finite endpoint set `S` has first signal `d` and bounded mass
+`a * ∑ w ∈ S, d w ≤ M`. At a floor `ρ > 0`, its heavy-set cardinality satisfies
+`#{w ∈ S | ρ / 4 < d w} * a * ρ ≤ 4 * M`, including at zero scale `a = 0`.
+Suppose that, on a finite slice of draws, every heavy endpoint other than one specified
+endpoint is retained on at most a
 `c * a` fraction of the draws. The specified endpoint can contribute one retained entry.
 Markov's inequality then bounds the fraction of draws retaining at least `n / 2` heavy
 entries by `2 * (1 + 4 * c * M) / (n * ρ)` when `ρ ≤ 1`.
@@ -39,6 +41,10 @@ integrated compression bound are separate steps.
 * `Cslib.Probability.card_filter_heavy_mul_le`: the deterministic heavy-set mass bound.
 * `Cslib.Probability.card_filter_heavyCountEvent_mul_le`: rarity without division.
 * `Cslib.Probability.card_filter_heavyCountEvent_le`: the explicit conditional rarity factor.
+* `Cslib.Probability.card_filter_heavyCountEvent_div_card_le`: the conditional frequency bound,
+  including empty slices.
+* `Cslib.Probability.card_filter_heavyCountEvent_product_div_card_le`: an independent start
+  slice preserves the frequency bound.
 
 ## References
 
@@ -54,62 +60,64 @@ open scoped BigOperators
 
 namespace Cslib.Probability
 
-variable {Ω V : Type*} [Fintype V]
+variable {Ω V : Type*}
 
 open Classical in
 /-- A true heavy count at floor `ρ`: at least half the capacity `n` consists of retained
-endpoints whose deterministic first signal exceeds `ρ / 4`. -/
-@[expose] def heavyCountEvent (Y : Ω → V → Prop) (d : V → ℝ) (ρ : ℝ) (n : ℕ)
+endpoints in `S` whose deterministic first signal exceeds `ρ / 4`. -/
+@[expose] def heavyCountEvent (Y : Ω → V → Prop) (S : Finset V) (d : V → ℝ) (ρ : ℝ) (n : ℕ)
     (σ : Ω) : Prop :=
-  n ≤ 2 * #{w | Y σ w ∧ ρ / 4 < d w}
+  n ≤ 2 * #{w ∈ S | Y σ w ∧ ρ / 4 < d w}
 
 /-- The deterministic mass bounds the number of entries above a quarter of the floor.
 The multiplied form remains valid at zero scale and for every floor. -/
-theorem card_filter_heavy_mul_le {a ρ M : ℝ} {d : V → ℝ} (ha : 0 ≤ a)
-    (hd : ∀ w, 0 ≤ d w) (hmass : a * ∑ w, d w ≤ M) :
-    (#{w | ρ / 4 < d w} : ℝ) * (a * ρ) ≤ 4 * M := by
+theorem card_filter_heavy_mul_le (S : Finset V) {a ρ M : ℝ} {d : V → ℝ} (ha : 0 ≤ a)
+    (hd : ∀ w ∈ S, 0 ≤ d w) (hmass : a * ∑ w ∈ S, d w ≤ M) :
+    (#{w ∈ S | ρ / 4 < d w} : ℝ) * (a * ρ) ≤ 4 * M := by
   classical
-  have hcount : (#{w | ρ / 4 < d w} : ℝ) * (ρ / 4) ≤ ∑ w, d w :=
-    card_filter_mul_le_sum univ _ d (fun w _ => hd w) fun _ _ hw => hw.le
+  have hcount : (#{w ∈ S | ρ / 4 < d w} : ℝ) * (ρ / 4) ≤ ∑ w ∈ S, d w :=
+    card_filter_mul_le_sum S _ d hd fun _ _ hw => hw.le
   have h := (mul_le_mul_of_nonneg_left hcount ha).trans hmass
   linarith
 
 open Classical in
 /-- Conditional rarity of a true heavy count, without division. The endpoint `y` may be
-forced by the conditioning slice, while all other endpoints satisfy its pair-count bound.
+forced by the conditioning slice, while only the other heavy endpoints need its pair-count bound.
 The slice and the capacity may be empty or zero. -/
-theorem card_filter_heavyCountEvent_mul_le (Y : Ω → V → Prop) (T : Finset Ω) (y : V)
-    {d : V → ℝ} {a ρ c M : ℝ} (ha : 0 < a) (hρ : 0 < ρ) (hc : 0 ≤ c)
-    (hd : ∀ w, 0 ≤ d w) (hmass : a * ∑ w, d w ≤ M)
-    (hpair : ∀ w, w ≠ y → (#{σ ∈ T | Y σ w} : ℝ) ≤ c * a * #T) (n : ℕ) :
-    (#{σ ∈ T | heavyCountEvent Y d ρ n σ} : ℝ) * n * ρ ≤
+theorem card_filter_heavyCountEvent_mul_le (Y : Ω → V → Prop) (T : Finset Ω)
+    (S : Finset V) (y : V) {d : V → ℝ} {a ρ c M : ℝ}
+    (ha : 0 ≤ a) (hρ : 0 < ρ) (hc : 0 ≤ c)
+    (hd : ∀ w ∈ S, 0 ≤ d w) (hmass : a * ∑ w ∈ S, d w ≤ M)
+    (hpair : ∀ w ∈ S, ρ / 4 < d w → w ≠ y →
+      (#{σ ∈ T | Y σ w} : ℝ) ≤ c * a * #T) (n : ℕ) :
+    (#{σ ∈ T | heavyCountEvent Y S d ρ n σ} : ℝ) * n * ρ ≤
       #T * (2 * (ρ + 4 * c * M)) := by
   classical
-  let D : Finset V := {w | ρ / 4 < d w}
+  let D : Finset V := {w ∈ S | ρ / 4 < d w}
   have hfilter (σ : Ω) : ({w ∈ D | Y σ w} : Finset V) =
-      ({w | Y σ w ∧ ρ / 4 < d w} : Finset V) := by
+      ({w ∈ S | Y σ w ∧ ρ / 4 < d w} : Finset V) := by
     ext w
-    simp [D, and_comm]
+    simp [D, and_left_comm, and_comm]
   have hevent (σ : Ω) : (n + 1) / 2 ≤ #{w ∈ D | Y σ w} ↔
-      heavyCountEvent Y d ρ n σ := by
+      heavyCountEvent Y S d ρ n σ := by
     rw [hfilter]
     unfold heavyCountEvent
     omega
-  have hcount := card_filter_le_card_filter_mul_le Y T D y (mul_nonneg hc ha.le)
-    (fun w _ hw => hpair w hw) ((n + 1) / 2)
+  have hcount := card_filter_le_card_filter_mul_le Y T D y (mul_nonneg hc ha)
+    (fun w hw hwy => hpair w (mem_filter.mp hw).1 (mem_filter.mp hw).2 hwy) ((n + 1) / 2)
   simp only [hevent] at hcount
   have hn : (n : ℝ) ≤ 2 * (((n + 1) / 2 : ℕ) : ℝ) := by
     exact_mod_cast (show n ≤ 2 * ((n + 1) / 2) by omega)
   have hmassD : (#D : ℝ) * (a * ρ) ≤ 4 * M :=
-    card_filter_heavy_mul_le ha.le hd hmass
+    card_filter_heavy_mul_le S ha hd hmass
   have hmassc : c * a * #D * ρ ≤ 4 * c * M := by
     have h := mul_le_mul_of_nonneg_left hmassD hc
     nlinarith
   calc
-    _ ≤ (#{σ ∈ T | heavyCountEvent Y d ρ n σ} : ℝ) *
+    _ ≤ (#{σ ∈ T | heavyCountEvent Y S d ρ n σ} : ℝ) *
         (2 * (((n + 1) / 2 : ℕ) : ℝ)) * ρ :=
       mul_le_mul_of_nonneg_right (mul_le_mul_of_nonneg_left hn (by positivity)) hρ.le
-    _ = 2 * ((#{σ ∈ T | heavyCountEvent Y d ρ n σ} : ℝ) *
+    _ = 2 * ((#{σ ∈ T | heavyCountEvent Y S d ρ n σ} : ℝ) *
         (((n + 1) / 2 : ℕ) : ℝ)) * ρ := by ring
     _ ≤ 2 * (#T * (1 + c * a * #D)) * ρ :=
       mul_le_mul_of_nonneg_right (mul_le_mul_of_nonneg_left hcount (by norm_num)) hρ.le
@@ -121,23 +129,67 @@ theorem card_filter_heavyCountEvent_mul_le (Y : Ω → V → Prop) (T : Finset 
 open Classical in
 /-- The conditional rarity factor `2 * (1 + 4 * c * M) / (n * ρ)` for a positive capacity
 and a floor in `(0, 1]`. Empty slices require no special convention. -/
-theorem card_filter_heavyCountEvent_le (Y : Ω → V → Prop) (T : Finset Ω) (y : V)
-    {d : V → ℝ} {a ρ c M : ℝ} (ha : 0 < a) (hρ : 0 < ρ) (hρ1 : ρ ≤ 1)
-    (hc : 0 ≤ c) (hd : ∀ w, 0 ≤ d w) (hmass : a * ∑ w, d w ≤ M)
-    (hpair : ∀ w, w ≠ y → (#{σ ∈ T | Y σ w} : ℝ) ≤ c * a * #T)
+theorem card_filter_heavyCountEvent_le (Y : Ω → V → Prop) (T : Finset Ω)
+    (S : Finset V) (y : V) {d : V → ℝ} {a ρ c M : ℝ}
+    (ha : 0 ≤ a) (hρ : 0 < ρ) (hρ1 : ρ ≤ 1)
+    (hc : 0 ≤ c) (hd : ∀ w ∈ S, 0 ≤ d w) (hmass : a * ∑ w ∈ S, d w ≤ M)
+    (hpair : ∀ w ∈ S, ρ / 4 < d w → w ≠ y →
+      (#{σ ∈ T | Y σ w} : ℝ) ≤ c * a * #T)
     {n : ℕ} (hn : 0 < n) :
-    (#{σ ∈ T | heavyCountEvent Y d ρ n σ} : ℝ) ≤
+    (#{σ ∈ T | heavyCountEvent Y S d ρ n σ} : ℝ) ≤
       (2 * (1 + 4 * c * M) / ((n : ℝ) * ρ)) * #T := by
   classical
-  have h := card_filter_heavyCountEvent_mul_le Y T y ha hρ hc hd hmass hpair n
+  have h := card_filter_heavyCountEvent_mul_le Y T S y ha hρ hc hd hmass hpair n
   have hn' : (0 : ℝ) < n := by exact_mod_cast hn
   rw [div_mul_eq_mul_div, le_div_iff₀ (mul_pos hn' hρ)]
   calc
-    _ = (#{σ ∈ T | heavyCountEvent Y d ρ n σ} : ℝ) * n * ρ := by ring
+    _ = (#{σ ∈ T | heavyCountEvent Y S d ρ n σ} : ℝ) * n * ρ := by ring
     _ ≤ #T * (2 * (ρ + 4 * c * M)) := h
     _ ≤ #T * (2 * (1 + 4 * c * M)) :=
       mul_le_mul_of_nonneg_left
         (mul_le_mul_of_nonneg_left (add_le_add hρ1 le_rfl) (by norm_num)) (by positivity)
     _ = _ := by ring
 
+open Classical in
+/-- The conditional true-heavy-count frequency bound. An empty conditioning slice has
+frequency zero, so no nonemptiness hypothesis is needed. -/
+theorem card_filter_heavyCountEvent_div_card_le (Y : Ω → V → Prop) (T : Finset Ω)
+    (S : Finset V) (y : V) {d : V → ℝ} {a ρ c M : ℝ}
+    (ha : 0 ≤ a) (hρ : 0 < ρ) (hρ1 : ρ ≤ 1) (hc : 0 ≤ c)
+    (hd : ∀ w ∈ S, 0 ≤ d w) (hmass : a * ∑ w ∈ S, d w ≤ M)
+    (hpair : ∀ w ∈ S, ρ / 4 < d w → w ≠ y →
+      (#{σ ∈ T | Y σ w} : ℝ) ≤ c * a * #T) {n : ℕ} (hn : 0 < n) :
+    (#{σ ∈ T | heavyCountEvent Y S d ρ n σ} : ℝ) / #T ≤
+      2 * (1 + 4 * c * M) / ((n : ℝ) * ρ) := by
+  classical
+  have hM : 0 ≤ M := (mul_nonneg ha (sum_nonneg hd)).trans hmass
+  rcases T.eq_empty_or_nonempty with rfl | hT
+  · simp only [filter_empty, card_empty, Nat.cast_zero, zero_div]
+    positivity
+  have hTpos : (0 : ℝ) < #T := by exact_mod_cast hT.card_pos
+  exact (div_le_iff₀ hTpos).mpr
+    (card_filter_heavyCountEvent_le Y T S y ha hρ hρ1 hc hd hmass hpair hn)
+
+open Classical in
+/-- Conditioning independently on a start seed preserves the heavy-count frequency bound.
+The actual product slice is used, and either of its two factors may be empty. -/
+theorem card_filter_heavyCountEvent_product_div_card_le {Γ : Type*}
+    (Y : Ω → V → Prop) (R : Finset Γ) (T : Finset Ω) (S : Finset V) (y : V)
+    {d : V → ℝ} {a ρ c M : ℝ} (ha : 0 ≤ a) (hρ : 0 < ρ) (hρ1 : ρ ≤ 1) (hc : 0 ≤ c)
+    (hd : ∀ w ∈ S, 0 ≤ d w) (hmass : a * ∑ w ∈ S, d w ≤ M)
+    (hpair : ∀ w ∈ S, ρ / 4 < d w → w ≠ y →
+      (#{σ ∈ T | Y σ w} : ℝ) ≤ c * a * #T) {n : ℕ} (hn : 0 < n) :
+    (#{σ ∈ R ×ˢ T | heavyCountEvent (fun σ w => Y σ.2 w) S d ρ n σ} : ℝ) / #(R ×ˢ T) ≤
+      2 * (1 + 4 * c * M) / ((n : ℝ) * ρ) := by
+  classical
+  refine card_filter_heavyCountEvent_div_card_le (fun (σ : Γ × Ω) w => Y σ.2 w)
+    (R ×ˢ T) S y ha hρ hρ1 hc hd hmass ?_ hn
+  intro w hw hdw hwy
+  have hset : {σ ∈ R ×ˢ T | Y σ.2 w} = R ×ˢ {σ ∈ T | Y σ w} := by
+    ext σ
+    simp [and_assoc]
+  rw [hset, card_product, card_product, Nat.cast_mul, Nat.cast_mul]
+  simpa only [mul_assoc, mul_comm, mul_left_comm] using
+    mul_le_mul_of_nonneg_left (hpair w hw hdw hwy) (Nat.cast_nonneg #R : (0 : ℝ) ≤ #R)
+
 end Cslib.Probability
diff --git a/Complexity/Foundations/Probability/HeavyCountRarity.lean b/Complexity/Foundations/Probability/HeavyCountRarity.lean
index e1891c7a33..0a307daa26 100644
--- a/Complexity/Foundations/Probability/HeavyCountRarity.lean
+++ b/Complexity/Foundations/Probability/HeavyCountRarity.lean
@@ -159,23 +159,23 @@ only the explicit conditional bound is used. This is the mean-error portion of
 [OpenAI2026LogSpace, Lemma 8.4], with an explicit constant and arbitrary positive exponent. -/
 theorem vertexNormPow_heavyCountEvent_le (hs : s ≠ 0) (hNu : 0 ≤ N * u)
     (X Y Yt : Ω → V → Prop) [∀ σ x, Decidable (X σ x)] [∀ σ y, Decidable (Yt σ y)]
-    {a ρ c M : ℝ} {n : ℕ} (ha : 0 < a) (hρ : 0 < ρ) (hρ1 : ρ ≤ 1)
+    {a ρ c M : ℝ} {n : ℕ} (ha : 0 ≤ a) (hρ : 0 < ρ) (hρ1 : ρ ≤ 1)
     (hc : 0 ≤ c) (hn : 0 < n) (d : V → V → ℝ) (hd : ∀ x y, 0 ≤ d x y)
     (hmass : ∀ x, a * ∑ y, d x y ≤ M)
-    (hpair : ∀ x y w, w ≠ y →
+    (hpair : ∀ x y w, ρ / 4 < d x w → w ≠ y →
       (#{σ | X σ x ∧ Yt σ y ∧ Y σ w} : ℝ) ≤
         c * a * #{σ | X σ x ∧ Yt σ y}) (b : V → V → ℝ) :
     vertexNormPow s N u X (fun σ x =>
-      if Probability.heavyCountEvent Y (d x) ρ n σ then
+      if Probability.heavyCountEvent Y univ (d x) ρ n σ then
         kthLargest 1 {y | Yt σ y} (fun y => |b x y|) else 0) ≤
       (2 * (1 + 4 * c * M) / ((n : ℝ) * ρ)) *
         rowNormPow s N u X Yt (fun _ x y => b x y) := by
   classical
   refine vertexNormPow_kthLargest_event_le hs hNu (fun x y => ?_) b
   have h := Probability.card_filter_heavyCountEvent_le Y
-    ({σ | X σ x ∧ Yt σ y} : Finset Ω) y ha hρ hρ1 hc (hd x) (hmass x)
-    (fun w hwy => ?_) hn
+    ({σ | X σ x ∧ Yt σ y} : Finset Ω) univ y ha hρ hρ1 hc (fun w _ => hd x w) (hmass x)
+    (fun w _ hdw hwy => ?_) hn
   · simpa only [filter_filter, and_assoc] using h
-  · simpa only [filter_filter, and_assoc] using hpair x y w hwy
+  · simpa only [filter_filter, and_assoc] using hpair x y w hdw hwy
 
 end Cslib
diff --git a/Complexity/Probability/PairwiseIndependentHash/HeavyCount.lean b/Complexity/Probability/PairwiseIndependentHash/HeavyCount.lean
index 65235d6604..118a15498b 100644
--- a/Complexity/Probability/PairwiseIndependentHash/HeavyCount.lean
+++ b/Complexity/Probability/PairwiseIndependentHash/HeavyCount.lean
@@ -28,6 +28,8 @@ allowed. This supplies the affine-channel instance of [OpenAI2026LogSpace, Lemma
 ## Main results
 
 * `Cslib.Probability.card_heavyCountEvent_affineRetains_le`: rarity after a narrower endpoint hit.
+* `Cslib.Probability.card_heavyCountEvent_affineRetains_div_card_le`: the corresponding
+  conditional frequency, including empty slices.
 
 ## References
 
@@ -45,13 +47,14 @@ namespace Cslib.Probability
 open Classical in
 /-- The true heavy count for the actual affine channel is rare even after conditioning on
 a hit at a narrower rate. Its nominal row-mass scale is `a ^ H`, not the box side `a`. -/
-theorem card_heavyCountEvent_affineRetains_le {V : Type*} [Fintype V] {P H : ℕ}
+theorem card_heavyCountEvent_affineRetains_le {V : Type*} (S : Finset V) {P H : ℕ}
     [Fact P.Prime] {ident : V → ZMod P} (hident : Function.Injective ident)
     {a : ℝ} (hPa : 1 ≤ P * a) (ha : a ≤ 1) {Lt : ℕ} (hLt : Lt ≤ ⌈P * a⌉₊)
     {d : V → ℝ} {ρ M : ℝ} (hρ : 0 < ρ) (hρ1 : ρ ≤ 1)
-    (hd : ∀ w, 0 ≤ d w) (hmass : a ^ H * ∑ w, d w ≤ M) {n : ℕ} (hn : 0 < n) (y : V) :
+    (hd : ∀ w ∈ S, 0 ≤ d w) (hmass : a ^ H * ∑ w ∈ S, d w ≤ M)
+    {n : ℕ} (hn : 0 < n) (y : V) :
     (#{s | affineRetains P H Lt s (ident y) ∧
-        heavyCountEvent (fun s w => affineRetains P H ⌈P * a⌉₊ s (ident w)) d ρ n s} : ℝ) ≤
+        heavyCountEvent (fun s w => affineRetains P H ⌈P * a⌉₊ s (ident w)) S d ρ n s} : ℝ) ≤
       (2 * (1 + 4 * (2 : ℝ) ^ H * M) / ((n : ℝ) * ρ)) *
         #{s | affineRetains P H Lt s (ident y)} := by
   classical
@@ -62,13 +65,45 @@ theorem card_heavyCountEvent_affineRetains_le {V : Type*} [Fintype V] {P H : ℕ
   have hLtP : Lt ≤ P := hLt.trans (affineRetains_rates (H := H) hPa ha).1
   simpa only [filter_filter] using card_filter_heavyCountEvent_le
     (fun s w => affineRetains P H ⌈P * a⌉₊ s (ident w))
-    ({s | affineRetains P H Lt s (ident y)} : Finset _) y
-    (pow_pos ha0 H) hρ hρ1 (by positivity : 0 ≤ (2 : ℝ) ^ H) hd hmass
-    (fun w hwy => by
+    ({s | affineRetains P H Lt s (ident y)} : Finset _) S y
+    (pow_nonneg ha0.le H) hρ hρ1 (by positivity : 0 ≤ (2 : ℝ) ^ H) hd hmass
+    (fun w _ _ hwy => by
       have h := card_affineRetains_and_affineRetains_le (H := H) hident hPa ha hLtP hwy
       convert h using 2
       congr 1
       ext s
       simp only [mem_filter, mem_univ, true_and]) hn
 
+open Classical in
+/-- The actual affine heavy-count frequency after a narrower endpoint hit. This is obtained
+from the count bound above, with zero frequency when the conditioning slice is empty. -/
+theorem card_heavyCountEvent_affineRetains_div_card_le {V : Type*} (S : Finset V) {P H : ℕ}
+    [Fact P.Prime] {ident : V → ZMod P} (hident : Function.Injective ident)
+    {a : ℝ} (hPa : 1 ≤ P * a) (ha : a ≤ 1) {Lt : ℕ} (hLt : Lt ≤ ⌈P * a⌉₊)
+    {d : V → ℝ} {ρ M : ℝ} (hρ : 0 < ρ) (hρ1 : ρ ≤ 1)
+    (hd : ∀ w ∈ S, 0 ≤ d w) (hmass : a ^ H * ∑ w ∈ S, d w ≤ M)
+    {n : ℕ} (hn : 0 < n) (y : V) :
+    (#{s ∈ ({s | affineRetains P H Lt s (ident y)} :
+        Finset (Matrix (Fin H) (Fin 1) (ZMod P) × (Fin H → ZMod P))) |
+      heavyCountEvent (fun s w => affineRetains P H ⌈P * a⌉₊ s (ident w)) S d ρ n s} : ℝ) /
+        #{s | affineRetains P H Lt s (ident y)} ≤
+      2 * (1 + 4 * (2 : ℝ) ^ H * M) / ((n : ℝ) * ρ) := by
+  classical
+  have ha0 : 0 ≤ a := by
+    by_contra h
+    have := mul_nonpos_of_nonneg_of_nonpos (Nat.cast_nonneg P) (not_le.mp h).le
+    linarith
+  have hM : 0 ≤ M := (mul_nonneg (pow_nonneg ha0 H) (sum_nonneg hd)).trans hmass
+  let T : Finset (Matrix (Fin H) (Fin 1) (ZMod P) × (Fin H → ZMod P)) :=
+    {s | affineRetains P H Lt s (ident y)}
+  change (#{s ∈ T | _} : ℝ) / #T ≤ _
+  rcases T.eq_empty_or_nonempty with hT | hT
+  · rw [hT]
+    simp only [filter_empty, card_empty, Nat.cast_zero, zero_div]
+    positivity
+  have hTpos : (0 : ℝ) < #T := by exact_mod_cast hT.card_pos
+  apply (div_le_iff₀ hTpos).mpr
+  simpa only [T, filter_filter] using
+    card_heavyCountEvent_affineRetains_le S hident hPa ha hLt hρ hρ1 hd hmass hn y
+
 end Cslib.Probability
diff --git a/ComplexityTests/CompressionHeavyCount.lean b/ComplexityTests/CompressionHeavyCount.lean
new file mode 100644
index 0000000000..4b3d30eaa1
--- /dev/null
+++ b/ComplexityTests/CompressionHeavyCount.lean
@@ -0,0 +1,223 @@
+/-
+Copyright (c) 2026 Samuel Schlesinger. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Samuel Schlesinger
+-/
+import Complexity.Probability.PairwiseIndependentHash.HeavyCount
+import Mathlib.Tactic.NormNum
+
+/-!
+# Tests for conditional heavy-count rarity
+
+Three off-endpoint hits are perfectly correlated: they all occur on one of eight draws.
+The distinguished endpoint is always retained. All four targets have value `1/2`, so with
+`a = 1/8`, `ρ = 1`, and capacity eight, the exceptional frequency is exactly `1/8` and the
+proved bound is `1/2 < 1`. An odd capacity exercises the ceiling in finite Markov.
+
+The affine example uses all seven field elements, broad side two and narrower endpoint side
+one. Its deterministic row is constantly `1/3`; the actual bound is `19/21 < 1`. The zero
+affine map is an exceptional seed in the conditioning slice, while the identity map belongs
+to the same slice and is not exceptional.
+
+A finite set of natural-number endpoints exercises the absence of a `Fintype` requirement.
+At zero scale, its always-retained light endpoint violates the old all-endpoint pair premise
+but does not affect the heavy count; the stronger division-free bound is attained exactly.
+-/
+
+namespace ComplexityTests.CompressionHeavyCount
+
+open Finset Cslib.Probability
+open scoped BigOperators
+
+private abbrev hit (σ : Fin 8) (y : Fin 4) : Prop := y = 0 ∨ σ = 0
+
+private theorem row_mass : (1 / 8 : ℝ) * ∑ _y : Fin 4, (1 / 2 : ℝ) ≤ 1 / 4 := by
+  norm_num
+
+private theorem pair_count (y : Fin 4) (_ : y ∈ (univ : Finset (Fin 4)))
+    (_ : (1 : ℝ) / 4 < 1 / 2) (hy : y ≠ 0) :
+    (#{σ ∈ (univ : Finset (Fin 8)) | hit σ y} : ℝ) ≤ 1 * (1 / 8) * #(univ : Finset (Fin 8)) := by
+  have hset : {σ ∈ (univ : Finset (Fin 8)) | hit σ y} = {0} := by
+    ext σ
+    simp [hit, hy]
+  rw [hset]
+  norm_num
+
+private theorem retained_heavy (σ : Fin 8) :
+    {y ∈ (univ : Finset (Fin 4)) | hit σ y ∧ (1 : ℝ) / 4 < 1 / 2} =
+      if σ = 0 then univ else {0} := by
+  by_cases hσ : σ = 0 <;> ext y <;> norm_num [hit, hσ]
+
+private theorem bad_seeds :
+    {σ ∈ (univ : Finset (Fin 8)) |
+      8 ≤ 2 * #{y ∈ (univ : Finset (Fin 4)) | hit σ y ∧ (1 : ℝ) / 4 < 1 / 2}} = {0} := by
+  ext σ
+  simp only [mem_filter, mem_univ, true_and, retained_heavy, mem_singleton]
+  by_cases hσ : σ = 0 <;> simp [hσ]
+
+-- Distinct off-endpoint hits are correlated, not independent Bernoulli trials.
+example : ({σ : Fin 8 | hit σ 1 ∧ hit σ 2} : Finset (Fin 8)) = {0} ∧
+    (1 / 8 : ℝ) ≠ (1 / 8) ^ 2 := by
+  constructor
+  · ext σ
+    norm_num [hit]
+  · norm_num
+
+example : (#{σ ∈ (univ : Finset (Fin 8)) |
+      8 ≤ 2 * #{y ∈ (univ : Finset (Fin 4)) | hit σ y ∧ (1 : ℝ) / 4 < 1 / 2}} : ℝ) /
+      #(univ : Finset (Fin 8)) = 1 / 8 := by
+  rw [bad_seeds]
+  norm_num
+
+-- The theorem consumes the actual row mass and off-endpoint pair counts.
+example : (#{σ ∈ (univ : Finset (Fin 8)) |
+      8 ≤ 2 * #{y ∈ (univ : Finset (Fin 4)) | hit σ y ∧ (1 : ℝ) / 4 < 1 / 2}} : ℝ) /
+      #(univ : Finset (Fin 8)) ≤ 1 / 2 ∧ (1 / 2 : ℝ) < 1 := by
+  have h := card_filter_heavyCountEvent_div_card_le hit univ univ 0
+    (d := fun _ => (1 / 2 : ℝ)) (a := 1 / 8) (c := 1) (ρ := 1) (M := 1 / 4)
+    (by norm_num) (by norm_num) (by norm_num) (by norm_num) (fun _ _ => by norm_num)
+    row_mass (by
+      intro w hw hdw hwy
+      convert pair_count w hw hdw hwy using 1
+      congr 2
+      ext σ
+      simp) (n := 8) (by decide)
+  norm_num [heavyCountEvent] at h ⊢
+  exact h
+
+example : (#{σ ∈ (univ : Finset (Fin 8)) |
+      7 ≤ 2 * #{y ∈ (univ : Finset (Fin 4)) | hit σ y ∧ (1 : ℝ) / 4 < 1 / 2}} : ℝ) /
+      #(univ : Finset (Fin 8)) ≤ 4 / 7 := by
+  have h := card_filter_heavyCountEvent_div_card_le hit univ univ 0
+    (d := fun _ => (1 / 2 : ℝ)) (a := 1 / 8) (c := 1) (ρ := 1) (M := 1 / 4)
+    (by norm_num) (by norm_num) (by norm_num) (by norm_num) (fun _ _ => by norm_num)
+    row_mass (by
+      intro w hw hdw hwy
+      convert pair_count w hw hdw hwy using 1
+      congr 2
+      ext σ
+      simp) (n := 7) (by decide)
+  norm_num [heavyCountEvent] at h ⊢
+  exact h
+
+-- A value exactly at the light/heavy threshold is not heavy.
+example : #{y ∈ (univ : Finset (Fin 4)) | (1 : ℝ) / 4 < if y = 0 then 1 / 4 else 1 / 2} = 3 := by
+  have hset : {y ∈ (univ : Finset (Fin 4)) |
+      (1 : ℝ) / 4 < if y = 0 then 1 / 4 else 1 / 2} = (univ : Finset (Fin 4)).erase 0 := by
+    ext y
+    by_cases hy : y = 0 <;> norm_num [hy]
+  rw [hset]
+  norm_num
+
+-- Either conditioning slice may be empty.
+example : (#{σ ∈ (∅ : Finset (Fin 8)) |
+      8 ≤ 2 * #{y ∈ (univ : Finset (Fin 4)) | hit σ y ∧ (1 : ℝ) / 4 < 1 / 2}} : ℝ) /
+      #(∅ : Finset (Fin 8)) ≤ 1 / 2 := by
+  have h := card_filter_heavyCountEvent_div_card_le hit ∅ univ 0
+    (d := fun _ => (1 / 2 : ℝ)) (a := 1 / 8) (c := 1) (ρ := 1) (M := 1 / 4)
+    (by norm_num) (by norm_num) (by norm_num) (by norm_num) (fun _ _ => by norm_num)
+    row_mass (fun _ _ _ _ => by simp) (n := 8) (by decide)
+  norm_num [heavyCountEvent] at h ⊢
+
+example (R : Finset Bool) :
+    (#{σ ∈ R ×ˢ (univ : Finset (Fin 8)) |
+      8 ≤ 2 * #{y ∈ (univ : Finset (Fin 4)) | hit σ.2 y ∧ (1 : ℝ) / 4 < 1 / 2}} : ℝ) /
+      #(R ×ˢ (univ : Finset (Fin 8))) ≤ 1 / 2 := by
+  have h := card_filter_heavyCountEvent_product_div_card_le hit R univ univ 0
+    (d := fun _ => (1 / 2 : ℝ)) (a := 1 / 8) (c := 1) (ρ := 1) (M := 1 / 4)
+    (by norm_num) (by norm_num) (by norm_num) (by norm_num) (fun _ _ => by norm_num)
+    row_mass (by
+      intro w hw hdw hwy
+      convert pair_count w hw hdw hwy using 1
+      congr 2
+      ext σ
+      simp) (n := 8) (by decide)
+  norm_num [heavyCountEvent] at h ⊢
+  exact h
+
+private instance : Fact (Nat.Prime 7) := ⟨by decide⟩
+
+private abbrev AffineSeed := Matrix (Fin 1) (Fin 1) (ZMod 7) × (Fin 1 → ZMod 7)
+private def narrowSlice : Finset AffineSeed := {σ | affineRetains 7 1 1 σ 0}
+private abbrev affineBad (σ : AffineSeed) : Prop :=
+  14 ≤ 2 * #({y : ZMod 7 | affineRetains 7 1 2 σ y} : Finset (ZMod 7))
+
+-- An actual affine specialization with a strictly narrower positive endpoint box.
+example : (#{σ ∈ narrowSlice | affineBad σ} : ℝ) / #narrowSlice ≤ 19 / 21 ∧
+    (19 / 21 : ℝ) < 1 := by
+  have h := card_heavyCountEvent_affineRetains_div_card_le (univ : Finset (ZMod 7))
+    Function.injective_id (H := 1) (a := (2 / 7 : ℝ)) (by norm_num) (by norm_num)
+    (Lt := 1) (by norm_num) (d := fun _ => (1 / 3 : ℝ)) (ρ := 1) (M := 2 / 3)
+    (by norm_num) (by norm_num) (fun _ _ => by norm_num) (by norm_num) (n := 14) (by decide) 0
+  norm_num [narrowSlice, affineBad, heavyCountEvent] at h ⊢
+  exact h
+
+-- The conditioning event and exceptional event are nonempty, while not all its seeds are bad.
+example : ((0, 0) : AffineSeed) ∈ narrowSlice ∧ affineBad (0, 0) := by
+  constructor
+  · decide
+  · decide
+
+example : ((fun _ _ => 1, 0) : AffineSeed) ∈ narrowSlice ∧
+    ¬ affineBad (fun _ _ => 1, 0) := by
+  constructor
+  · decide
+  · decide
+
+private abbrev finiteHits (_ : Unit) (_ : ℕ) : Prop := True
+private def finiteSignal (w : ℕ) : ℝ := if w = 1 then 0 else 1
+
+private theorem zero_scale_pair {ρ : ℝ} (hρ : 0 ≤ ρ) (w : ℕ) (hw : w ∈ ({0, 1} : Finset ℕ))
+    (hd : ρ / 4 < finiteSignal w) (hw0 : w ≠ 0) :
+    (#{σ ∈ (univ : Finset Unit) | finiteHits σ w} : ℝ) ≤ 0 * 0 * #(univ : Finset Unit) := by
+  rcases mem_insert.mp hw with hw | hw
+  · exact (hw0 hw).elim
+  · have hw1 := mem_singleton.mp hw
+    subst w
+    norm_num [finiteSignal] at hd
+    linarith
+
+-- A nonempty heavy event over a finite subset of an infinite endpoint type; only zero is heavy.
+example : heavyCountEvent finiteHits {0, 1} finiteSignal (1 / 2) 2 () ∧
+    ¬ heavyCountEvent finiteHits {0, 1} finiteSignal (1 / 2) 3 () := by
+  norm_num [heavyCountEvent, finiteHits, finiteSignal, filter_insert, filter_singleton]
+
+-- Requiring the pair bound at the light endpoint one would rule this instance out.
+example : ¬ (#{σ ∈ (univ : Finset Unit) | finiteHits σ 1} : ℝ) ≤
+    0 * 0 * #(univ : Finset Unit) := by
+  norm_num [finiteHits]
+
+-- The original stronger bound has RHS one, while replacing ρ by one would give RHS two.
+open scoped Classical in
+example : (#{σ ∈ (univ : Finset Unit) |
+      heavyCountEvent finiteHits {0, 1} finiteSignal (1 / 2) 2 σ} : ℝ) * 2 * (1 / 2) ≤ 1 := by
+  have h := card_filter_heavyCountEvent_mul_le finiteHits univ {0, 1} 0
+    (d := finiteSignal) (a := 0) (ρ := 1 / 2) (c := 0) (M := 0)
+    (by norm_num) (by norm_num) (by norm_num)
+    (fun w _ => by unfold finiteSignal; split_ifs <;> norm_num) (by simp)
+    (by
+      intro w hw hdw hwy
+      convert zero_scale_pair (ρ := 1 / 2) (by norm_num) w hw hdw hwy using 1
+      congr 2
+      ext σ
+      simp) 2
+  norm_num at h ⊢
+  exact h
+
+open scoped Classical in
+example : (#{σ ∈ (univ : Finset Unit) |
+      heavyCountEvent finiteHits {0, 1} finiteSignal 1 2 σ} : ℝ) / #(univ : Finset Unit) ≤ 1 := by
+  have h := card_filter_heavyCountEvent_div_card_le finiteHits univ {0, 1} 0
+    (d := finiteSignal) (a := 0) (ρ := 1) (c := 0) (M := 0)
+    (by norm_num) (by norm_num) (by norm_num) (by norm_num)
+    (fun w _ => by unfold finiteSignal; split_ifs <;> norm_num) (by simp)
+    (by
+      intro w hw hdw hwy
+      convert zero_scale_pair (ρ := 1) (by norm_num) w hw hdw hwy using 1
+      congr 2
+      ext σ
+      simp) (n := 2) (by decide)
+  norm_num at h ⊢
+  exact h
+
+end ComplexityTests.CompressionHeavyCount
diff --git a/ComplexityTests/HeavyCountRarity.lean b/ComplexityTests/HeavyCountRarity.lean
index 123f9aed24..fe5cd83e1b 100644
--- a/ComplexityTests/HeavyCountRarity.lean
+++ b/ComplexityTests/HeavyCountRarity.lean
@@ -29,7 +29,7 @@ example : ({σ | correlated σ 1 ∧ correlated σ 2} : Finset (Fin 5)) = {0} :=
   decide
 
 private theorem heavy_iff (σ : Fin 5) :
-    heavyCountEvent correlated (fun _ => 1 / 3) 1 8 σ ↔ σ = 0 := by
+    heavyCountEvent correlated univ (fun _ => 1 / 3) 1 8 σ ↔ σ = 0 := by
   classical
   by_cases hσ : σ = 0
   · subst σ
@@ -41,9 +41,9 @@ private theorem heavy_iff (σ : Fin 5) :
 
 -- The rare event has positive probability, and the explicit upper bound is below one.
 open scoped Classical in
-example : (dens {σ | heavyCountEvent correlated (fun _ => 1 / 3) 1 8 σ} : ℝ) = 1 / 5 := by
+example : (dens {σ | heavyCountEvent correlated univ (fun _ => 1 / 3) 1 8 σ} : ℝ) = 1 / 5 := by
   classical
-  have hevent : ({σ | heavyCountEvent correlated (fun _ => 1 / 3) 1 8 σ} :
+  have hevent : ({σ | heavyCountEvent correlated univ (fun _ => 1 / 3) 1 8 σ} :
       Finset (Fin 5)) = {0} := by
     ext σ
     simp only [mem_filter, mem_univ, true_and, mem_singleton]
@@ -52,7 +52,7 @@ example : (dens {σ | heavyCountEvent correlated (fun _ => 1 / 3) 1 8 σ} : ℝ)
   norm_num
 
 open scoped Classical in
-example : (#{σ : Fin 5 | heavyCountEvent correlated (fun _ => 1 / 3) 1 8 σ} : ℝ) ≤
+example : (#{σ : Fin 5 | heavyCountEvent correlated univ (fun _ => 1 / 3) 1 8 σ} : ℝ) ≤
     (7 / 12) * Fintype.card (Fin 5) := by
   classical
   have hpair : ∀ y : Fin 5, y ≠ 0 →
@@ -63,13 +63,12 @@ example : (#{σ : Fin 5 | heavyCountEvent correlated (fun _ => 1 / 3) 1 8 σ} :
       ext σ
       simp [correlated, hy]
     norm_num [hs]
-  have h := @card_filter_heavyCountEvent_le (Fin 5) (Fin 5) (inferInstance : Fintype (Fin 5))
-    correlated univ (0 : Fin 5)
+  have h := card_filter_heavyCountEvent_le correlated univ univ (0 : Fin 5)
     (a := 1 / 5) (ρ := 1) (c := 1) (M := 1 / 3) (d := fun _ => 1 / 3)
     (by norm_num) (by norm_num) (by norm_num) (by norm_num)
-    (fun _ => by norm_num) (by norm_num)
+    (fun _ _ => by norm_num) (by norm_num)
     (by
-      intro w hw
+      intro w _ _ hw
       convert hpair w hw using 1
       congr 2
       ext σ
@@ -79,17 +78,17 @@ example : (#{σ : Fin 5 | heavyCountEvent correlated (fun _ => 1 / 3) 1 8 σ} :
 
 -- An odd capacity requires rounding up; equality with the heavy threshold is excluded.
 example : ¬ heavyCountEvent (fun (_ : Unit) (y : Fin 3) => y = 0)
-    (fun _ => 1) 1 3 () := by
+    univ (fun _ => 1) 1 3 () := by
   classical
   norm_num [heavyCountEvent, show ({y : Fin 3 | y = 0} : Finset (Fin 3)) = {0} by decide]
 
 example : heavyCountEvent (fun (_ : Unit) (y : Fin 3) => y ≠ 2)
-    (fun _ => 1) 1 3 () := by
+    univ (fun _ => 1) 1 3 () := by
   classical
   norm_num [heavyCountEvent, show ({y : Fin 3 | y ≠ 2} : Finset (Fin 3)) = {0, 1} by decide]
 
 example : ¬ heavyCountEvent (fun (_ : Unit) (_ : Fin 3) => True)
-    (fun _ => 1 / 4) 1 1 () := by
+    univ (fun _ => 1 / 4) 1 1 () := by
   classical
   norm_num [heavyCountEvent]
 
@@ -184,14 +183,14 @@ private instance : Fact (Nat.Prime 5) := ⟨by decide⟩
 open scoped Classical in
 example :
     (#{σ | affineRetains 5 1 1 σ 0 ∧ heavyCountEvent
-      (fun σ (y : ZMod 5) => affineRetains 5 1 1 σ y) (fun _ => 1 / 3) 1 8 σ} : ℝ) ≤
+      (fun σ (y : ZMod 5) => affineRetains 5 1 1 σ y) univ (fun _ => 1 / 3) 1 8 σ} : ℝ) ≤
       (11 / 12) * #{σ | affineRetains 5 1 1 σ 0} := by
   classical
-  have h := card_heavyCountEvent_affineRetains_le
+  have h := card_heavyCountEvent_affineRetains_le univ
     (V := ZMod 5) (P := 5) (H := 1) (ident := id) Function.injective_id
     (a := 1 / 5) (by norm_num) (by norm_num) (Lt := 1) (by norm_num)
     (d := fun _ => 1 / 3) (ρ := 1) (M := 1 / 3)
-    (by norm_num) (by norm_num) (fun _ => by norm_num) (by norm_num)
+    (by norm_num) (by norm_num) (fun _ _ => by norm_num) (by norm_num)
     (n := 8) (by decide) 0
   norm_num at h ⊢
   exact h
@@ -202,7 +201,7 @@ private abbrev forced (_ : Fin 5) (y : Fin 5) : Prop := y = 0
 open scoped Classical in
 example :
     vertexNormPow 4 5 1 (fun (_ _ : Fin 5) => True) (fun σ _ =>
-      if heavyCountEvent correlated (fun _ => 1 / 3) 1 8 σ then
+      if heavyCountEvent correlated univ (fun _ => 1 / 3) 1 8 σ then
         kthLargest 1 {y | forced σ y} (fun _ => |(2 : ℝ)|) else 0) ≤
       (7 / 12) * rowNormPow 4 5 1 (fun (_ _ : Fin 5) => True) forced (fun _ _ _ => 2) := by
   classical
@@ -224,7 +223,7 @@ example :
     (by norm_num) (by norm_num) (by norm_num) (by norm_num) (by decide)
     (fun _ _ => 1 / 3) (fun _ _ => by norm_num) (fun _ => by norm_num)
     (by
-      intro x y w hwy
+      intro x y w _ hwy
       convert hpair x y w hwy using 1
       congr 2
       ext σ