From 7bd15cd3d7945cdbebdb5fc464d1deaf25ecb565 Mon Sep 17 00:00:00 2001
From: Samuel Schlesinger <samschlesinger@google.com>
Date: Sat, 24 Oct 2026 06:48:44 +0000
Subject: [PATCH 1/2] refactor(foundations): move general arithmetic and
 counting lemmas out of Classes (#610)

---
 .../Complexity/Classes/Toda/Counting.lean     |  95 +---------
 .../Complexity/Classes/Toda/Isolation.lean    |  77 +-------
 .../Complexity/Problems/SubsetSum/Digits.lean |  58 +++---
 .../Kolmogorov/Incompressibility.lean         |  26 +--
 .../Computability/Kolmogorov/Partrec.lean     |  10 +-
 .../Computability/PCP/DegreeReduction.lean    |  17 +-
 .../Computability/USTCON/Reader/Correct.lean  |  13 +-
 .../USTCON/Reader/Invariant.lean              |   4 +-
 .../Data/BitString/ShortWords.lean            |  18 ++
 .../Foundations/Data/BitString/WordCount.lean | 168 ++++++++++++++++++
 .../Foundations/Data/Finset/Quantile.lean     |  18 ++
 Complexity/Foundations/Data/Nat/Bits.lean     |  22 ++-
 12 files changed, 264 insertions(+), 262 deletions(-)

diff --git a/Complexity/Computability/Complexity/Classes/Toda/Counting.lean b/Complexity/Computability/Complexity/Classes/Toda/Counting.lean
index 24da400d83..14f55edec7 100644
--- a/Complexity/Computability/Complexity/Classes/Toda/Counting.lean
+++ b/Complexity/Computability/Complexity/Classes/Toda/Counting.lean
@@ -17,9 +17,7 @@ import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Bi
 import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.List
 import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Nat
 import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Nat.Div
-import Mathlib.Data.Finset.Sort
 import Mathlib.Data.List.GetD
-import Mathlib.Data.Nat.Choose.Sum
 
 /-!
 # Counting the parities of a random string with one bit of a `#P` value
@@ -34,16 +32,16 @@ Toda's amplifier uses residues `0` modulo `2 ^ K` for even counts and `-1` for o
 This module uses the opposite sign: `0` for even counts and `+1` for odd counts. Negating our
 amplifier modulo `2 ^ K` recovers the `0`/`-1` convention. All subsequent counts and bit
 extraction here use the `+1` convention, from the binomial expansion of `(1 - 2) ^ c`
-(`Cslib.Complexity.Toda.sum_range_neg_two_pow_mul_choose`):
+(`Cslib.BitString.sum_range_neg_two_pow_mul_choose`):
 
 `[c odd] = ∑ i < c, (-2) ^ i * choose c (i + 1)`,
 
 whose terms with `i ≥ K` vanish modulo `2 ^ K`
-(`Cslib.Complexity.Toda.sum_range_neg_two_pow_mul_choose_zmod`). The coefficients `(-2) ^ i` are
+(`Cslib.BitString.sum_range_neg_two_pow_mul_choose_zmod`). The coefficients `(-2) ^ i` are
 replaced by naturals equal to them modulo `2 ^ K` (`Cslib.Complexity.Toda.parityCoeff`), and
 `choose (f r) k` counts the `k`-element sets of accepted witnesses, written as strictly
 increasing lists of `k` words for the lexicographic order
-(`Cslib.Complexity.Toda.card_filter_strictMono`, `Cslib.BitString.wordLt_ofFn_iff`). So
+(`Cslib.BitString.card_filter_strictMono`, `Cslib.BitString.wordLt_ofFn_iff`). So
 the words accepted by `Cslib.Complexity.Toda.countingTest` — a size `k ≤ K` in unary, one of
 `parityCoeff K (k - 1)` coefficient words, a random string `r` and a strictly increasing list of
 `k` accepted witnesses, padded with zero words — number
@@ -66,9 +64,6 @@ odd number of accepted witnesses (`Cslib.Complexity.Toda.testBit_card_filter_sha
 
 ## Main results
 
-* `Cslib.Complexity.Toda.sum_range_neg_two_pow_mul_choose_zmod`: the parity of `c` from binomial
-  coefficients, modulo `2 ^ K`.
-* `Cslib.Complexity.Toda.card_filter_strictMono`: strictly increasing tuples count subsets.
 * `Cslib.Complexity.Toda.cast_card_filter_countingTest`: the count is `G` modulo `2 ^ (R + 1)`.
 * `Cslib.Complexity.Toda.testBit_card_filter_sharpTest`: one bit says whether `2 G > 2 ^ R`.
 
@@ -82,55 +77,10 @@ odd number of accepted witnesses (`Cslib.Complexity.Toda.testBit_card_filter_sha
 
 namespace Cslib.Complexity.Toda
 
-open Finset Turing.MultiTapeTM
+open Finset BitString Turing.MultiTapeTM
 
 /-! ### Modulus amplification -/
 
-/-- **The parity of `c` from the binomial expansion of `(1 - 2) ^ c`**:
-`∑ i < c, (-2) ^ i * choose c (i + 1)` is `1` for odd `c` and `0` for even `c`. -/
-theorem sum_range_neg_two_pow_mul_choose (c : ℕ) :
-    ∑ i ∈ range c, (-2 : ℤ) ^ i * (c.choose (i + 1) : ℤ) = if Odd c then 1 else 0 := by
-  have hbin : ∑ i ∈ range (c + 1), (-2 : ℤ) ^ i * (c.choose i : ℤ) = (-1) ^ c := by
-    have := add_pow (-2 : ℤ) 1 c
-    simp only [one_pow, mul_one] at this
-    rw [show (-2 : ℤ) + 1 = -1 by norm_num] at this
-    rw [this]
-  rw [sum_range_succ'] at hbin
-  simp only [pow_zero, Nat.choose_zero_right, Nat.cast_one, mul_one] at hbin
-  have h : -2 * ∑ i ∈ range c, (-2 : ℤ) ^ i * (c.choose (i + 1) : ℤ) = (-1) ^ c - 1 := by
-    rw [mul_sum]
-    rw [← hbin]
-    simp only [pow_succ]
-    ring_nf
-  split
-  · rename_i hc
-    rw [hc.neg_one_pow] at h
-    linarith
-  · rename_i hc
-    rw [(Nat.not_odd_iff_even.1 hc).neg_one_pow, sub_self] at h
-    linarith
-
-/-- **The parity of `c` modulo `2 ^ K`**: only the first `K` binomial terms matter. -/
-theorem sum_range_neg_two_pow_mul_choose_zmod (c K : ℕ) :
-    ∑ i ∈ range K, (-2 : ZMod (2 ^ K)) ^ i * (c.choose (i + 1) : ZMod (2 ^ K)) =
-      if Odd c then 1 else 0 := by
-  have hexact := congrArg (Int.cast : ℤ → ZMod (2 ^ K)) (sum_range_neg_two_pow_mul_choose c)
-  push_cast at hexact
-  rw [← hexact]
-  have hK : (-2 : ZMod (2 ^ K)) ^ K = 0 := by
-    have h2 : (2 : ZMod (2 ^ K)) ^ K = 0 := by
-      exact_mod_cast ZMod.natCast_self (2 ^ K)
-    rw [neg_pow, h2, mul_zero]
-  have h₁ : ∑ i ∈ range (K + c), (-2 : ZMod (2 ^ K)) ^ i * (c.choose (i + 1) : ZMod (2 ^ K)) =
-      ∑ i ∈ range K, (-2 : ZMod (2 ^ K)) ^ i * (c.choose (i + 1) : ZMod (2 ^ K)) := by
-    rw [sum_range_add]
-    simp [pow_add, hK]
-  have h₂ : ∑ i ∈ range (c + K), (-2 : ZMod (2 ^ K)) ^ i * (c.choose (i + 1) : ZMod (2 ^ K)) =
-      ∑ i ∈ range c, (-2 : ZMod (2 ^ K)) ^ i * (c.choose (i + 1) : ZMod (2 ^ K)) := by
-    rw [sum_range_add]
-    simp [Nat.choose_eq_zero_of_lt (by omega : c < c + _ + 1)]
-  rw [← h₁, ← h₂, Nat.add_comm]
-
 /-- Natural coefficients equal to `(-2) ^ i` modulo `2 ^ K`, for `i ≤ K`: `2 ^ i` for even `i`
 and `2 ^ K - 2 ^ i` for odd `i`. -/
 def parityCoeff (K i : ℕ) : ℕ := if Even i then 2 ^ i else 2 ^ K - 2 ^ i
@@ -184,43 +134,6 @@ private theorem testBit_two_mul_add_two_pow_sub_one {R G H : ℕ} (hG : G ≤ 2
 
 /-! ### Subsets as strictly increasing tuples -/
 
-/-- **Strictly increasing tuples count subsets**: the strictly increasing `k`-tuples of elements
-of `A` are as many as the `k`-element subsets of `A`. -/
-theorem card_filter_strictMono {β : Type*} [LinearOrder β] [Fintype β] (A : Finset β) (k : ℕ)
-    [DecidablePred fun g : Fin k → β => StrictMono g ∧ ∀ i, g i ∈ A] :
-    (univ.filter fun g : Fin k → β => StrictMono g ∧ ∀ i, g i ∈ A).card = (#A).choose k := by
-  classical
-  rw [← card_powersetCard]
-  refine card_bij (fun g _ => univ.image g) ?_ ?_ ?_
-  · intro g hg
-    simp only [mem_filter, mem_univ, true_and] at hg
-    rw [mem_powersetCard]
-    refine ⟨fun x hx => ?_, ?_⟩
-    · obtain ⟨i, -, rfl⟩ := mem_image.1 hx
-      exact hg.2 i
-    · rw [card_image_of_injective _ hg.1.injective, card_univ, Fintype.card_fin]
-  · intro g hg g' hg' h
-    simp only [mem_filter, mem_univ, true_and] at hg hg'
-    have hc : (univ.image g).card = k := by
-      rw [card_image_of_injective _ hg.1.injective, card_univ, Fintype.card_fin]
-    have h1 : g = (univ.image g).orderEmbOfFin hc :=
-      orderEmbOfFin_unique hc (fun i => mem_image_of_mem g (mem_univ i)) hg.1
-    have h2 : g' = (univ.image g).orderEmbOfFin hc :=
-      orderEmbOfFin_unique hc (fun i => h ▸ mem_image_of_mem g' (mem_univ i)) hg'.1
-    rw [h1, ← h2]
-  · intro s hs
-    rw [mem_powersetCard] at hs
-    refine ⟨s.orderEmbOfFin hs.2, ?_, image_orderEmbOfFin_univ s hs.2⟩
-    simp only [mem_filter, mem_univ, true_and]
-    exact ⟨(s.orderEmbOfFin hs.2).strictMono, fun i => hs.1 (orderEmbOfFin_mem s hs.2 i)⟩
-
-/-- A tuple increasing at every step is strictly increasing. -/
-private theorem strictMono_of_lt_succ {β : Type*} [Preorder β] {k : ℕ} {g : Fin k → β}
-    (h : ∀ (i : ℕ) (hi : i + 1 < k), g ⟨i, by omega⟩ < g ⟨i + 1, hi⟩) : StrictMono g := by
-  cases k with
-  | zero => exact fun i => i.elim0
-  | succ k => exact Fin.strictMono_iff_lt_succ.2 fun i => h i (by omega)
-
 /-- The `k`-subset test on `K` rows of `Z` bits: the first `k` rows are accepted by `acc` and
 strictly increasing, and the other rows are zero. -/
 def subsetTest (acc : List Bool → Bool) (K Z k : ℕ) (zs : List Bool) : Bool :=
diff --git a/Complexity/Computability/Complexity/Classes/Toda/Isolation.lean b/Complexity/Computability/Complexity/Classes/Toda/Isolation.lean
index 4e5271013d..d26eb77473 100644
--- a/Complexity/Computability/Complexity/Classes/Toda/Isolation.lean
+++ b/Complexity/Computability/Complexity/Classes/Toda/Isolation.lean
@@ -39,7 +39,7 @@ A *trial* sums the numbers `c x` over the strings `x` passing the test of some l
 seed; its parity is the parity of the number of `x` with `c x` odd that pass the test
 (`Finset.odd_sum_iff_odd_card_odd`). The trials are combined by the parity form of a
 disjunction: `1 + ∏ⱼ (1 + cⱼ)` is odd exactly when some `cⱼ` is
-(`Cslib.Complexity.Toda.odd_one_add_prod_one_add`). Running `4 (E + 1)` rounds, each with one
+(`Cslib.BitString.odd_one_add_prod_one_add`). Running `4 (E + 1)` rounds, each with one
 trial at every level `k ≤ M + 2`, the combined number is odd exactly when `S` is nonempty, unless
 some `c x` has the wrong parity or every round fails to isolate an element of `S`
 (`Cslib.Complexity.Toda.two_pow_mul_card_filter_not_odd_iff_le`). With `c x` depending on
@@ -54,7 +54,6 @@ first failure has probability at most `2 ^ M * 2 ^ (-(E + M + 1))`, the second a
 
 ## Main results
 
-* `Cslib.Complexity.Toda.odd_one_add_prod_one_add`: the parity form of a disjunction.
 * `Cslib.Complexity.Toda.hashesToZero_ofFn_iff`: the test is the affine hash hitting `0`.
 * `Cslib.Complexity.Toda.three_mul_two_pow_le_card_filter_card_eq_one`: isolation with
   probability at least `3 / 16`.
@@ -73,58 +72,7 @@ first failure has probability at most `2 ^ M * 2 ^ (-(E + M + 1))`, the second a
 
 namespace Cslib.Complexity.Toda
 
-open Finset Turing.MultiTapeTM
-
-/-! ### Counting words -/
-
-/-- A product of naturals is odd exactly when every factor is. -/
-theorem odd_prod_iff {ι : Type*} {s : Finset ι} (f : ι → ℕ) :
-    Odd (∏ j ∈ s, f j) ↔ ∀ j ∈ s, Odd (f j) := by
-  classical
-  induction s using Finset.induction_on with
-  | empty => simp
-  | insert a s ha ih => rw [Finset.prod_insert ha, Nat.odd_mul, ih, Finset.forall_mem_insert]
-
-/-- **The parity form of a disjunction**: `1 + ∏ⱼ (1 + cⱼ)` is odd exactly when some `cⱼ` is
-odd. -/
-theorem odd_one_add_prod_one_add {ι : Type*} [Fintype ι] (c : ι → ℕ) :
-    Odd (1 + ∏ j, (1 + c j)) ↔ ∃ j, Odd (c j) := by
-  rw [Nat.add_comm, Nat.odd_add_one, odd_prod_iff]
-  simp only [mem_univ, true_imp_iff, not_forall]
-  refine exists_congr fun j => ?_
-  rw [Nat.add_comm, Nat.odd_add_one, not_not]
-
-/-- The functions `s : ι → X` whose values at the `t` distinct points `f i` lie in `F`: `F` is
-chosen at those points and anything elsewhere. -/
-private theorem card_filter_forall_apply_mem {ι X : Type*} [Fintype ι] [DecidableEq ι] [Fintype X]
-    [DecidableEq X] {t : ℕ} (f : Fin t → ι) (hf : Function.Injective f) (F : Finset X) :
-    (univ.filter fun s : ι → X => ∀ i, s (f i) ∈ F).card =
-      #F ^ t * Fintype.card X ^ (Fintype.card ι - t) := by
-  classical
-  have h : (univ.filter fun s : ι → X => ∀ i, s (f i) ∈ F) =
-      Fintype.piFinset fun j => if j ∈ Finset.image f univ then F else univ := by
-    ext s
-    simp only [mem_filter, mem_univ, true_and, Fintype.mem_piFinset]
-    constructor
-    · intro hs j
-      split
-      · rename_i hj
-        obtain ⟨i, -, rfl⟩ := Finset.mem_image.1 hj
-        exact hs i
-      · exact mem_univ _
-    · intro hs i
-      have := hs (f i)
-      rwa [ite_eq_left_iff.2 (fun h => absurd (Finset.mem_image_of_mem f (mem_univ i)) h)]
-        at this
-  rw [h, Fintype.card_piFinset]
-  simp only [apply_ite Finset.card, card_univ]
-  rw [Finset.prod_ite, Finset.prod_const, Finset.prod_const]
-  have himg : (univ.filter fun j => j ∈ Finset.image f univ) = Finset.image f univ := by
-    ext j; simp
-  have hcard : #(Finset.image f univ) = t := by
-    rw [Finset.card_image_of_injective _ hf, card_univ, Fintype.card_fin]
-  rw [himg, hcard, Finset.filter_not, himg, Finset.card_sdiff_of_subset (subset_univ _), hcard,
-    card_univ]
+open Finset BitString Turing.MultiTapeTM
 
 /-! ### The Valiant–Vazirani test -/
 
@@ -247,27 +195,6 @@ private theorem two_pow_mul_thirteen_pow_le (E : ℕ) :
   rw [pow_mul, pow_mul, ← mul_pow]
   exact Nat.pow_le_pow_left (by norm_num) _
 
-/-- **The union bound for random strings**: if each `x` is bad for at most a `2 ^ (-e')` fraction
-of the random strings, some `x` of length `M` is bad for at most a `2 ^ (M - e')` fraction. -/
-private theorem two_pow_mul_card_filter_exists_le {R M e' : ℕ}
-    {Bad : (Fin R → Bool) → (Fin M → Bool) → Prop}
-    [∀ r x, Decidable (Bad r x)]
-    (h : ∀ x, 2 ^ e' * (univ.filter fun r => Bad r x).card ≤ 2 ^ R) :
-    2 ^ e' * (univ.filter fun r => ∃ x, Bad r x).card ≤ 2 ^ M * 2 ^ R := by
-  classical
-  have hsub : (univ.filter fun r => ∃ x, Bad r x) ⊆
-      univ.biUnion fun x => univ.filter fun r => Bad r x := by
-    intro r hr
-    simp only [mem_filter, mem_univ, true_and] at hr
-    obtain ⟨x, hx⟩ := hr
-    exact mem_biUnion.2 ⟨x, mem_univ _, by simpa using hx⟩
-  calc 2 ^ e' * (univ.filter fun r => ∃ x, Bad r x).card
-      ≤ 2 ^ e' * ∑ x, (univ.filter fun r => Bad r x).card :=
-        Nat.mul_le_mul_left _ ((card_le_card hsub).trans card_biUnion_le)
-    _ = ∑ x : Fin M → Bool, 2 ^ e' * (univ.filter fun r => Bad r x).card := mul_sum ..
-    _ ≤ ∑ _x : Fin M → Bool, 2 ^ R := sum_le_sum fun x _ => h x
-    _ = 2 ^ M * 2 ^ R := by simp
-
 /-- **The isolation step errs with probability at most `2 ^ (-E)`.** Let `c r x` be numbers
 whose parity says whether `x ∈ S`, except for at most a `2 ^ (-e')` fraction of the random
 strings `r` of length `R`, for each string `x` of length `M`, where `e' ≥ E + M + 1`. Draw seeds
diff --git a/Complexity/Computability/Complexity/Problems/SubsetSum/Digits.lean b/Complexity/Computability/Complexity/Problems/SubsetSum/Digits.lean
index 6a19b8f9e4..69a7293aaf 100644
--- a/Complexity/Computability/Complexity/Problems/SubsetSum/Digits.lean
+++ b/Complexity/Computability/Complexity/Problems/SubsetSum/Digits.lean
@@ -11,6 +11,7 @@ public import Complexity.Init
 public import Mathlib.Algebra.BigOperators.Group.Finset.Basic
 public import Mathlib.Algebra.Order.BigOperators.Group.Finset
 import Mathlib.Algebra.BigOperators.Ring.Finset
+import Mathlib.Data.Nat.Digits.Defs
 import Mathlib.Tactic.Ring
 
 /-!
@@ -40,49 +41,36 @@ open Finset
 
 namespace Nat
 
+private theorem sum_range_mul_pow_eq_ofDigits (b N : ℕ) (a : ℕ → ℕ) :
+    ∑ p ∈ range N, a p * b ^ p = ofDigits b ((List.range N).map a) := by
+  induction N with
+  | zero => rfl
+  | succ N ih =>
+    rw [sum_range_succ, ih, List.range_succ, List.map_append, List.map_singleton, ofDigits_append]
+    simp [mul_comm]
+
 /-- Base-`b` digits that are less than `b` are determined by the number they represent. -/
 theorem sum_range_mul_pow_inj {b N : ℕ} {a c : ℕ → ℕ} (ha : ∀ p < N, a p < b)
     (hc : ∀ p < N, c p < b) :
     ∑ p ∈ range N, a p * b ^ p = ∑ p ∈ range N, c p * b ^ p ↔ ∀ p < N, a p = c p := by
-  refine ⟨fun h => ?_, fun h => sum_congr rfl fun p hp => by rw [h p (mem_range.1 hp)]⟩
-  induction N generalizing a c with
-  | zero => simp
-  | succ N ih =>
-    have hb : 0 < b := (Nat.zero_le _).trans_lt (ha 0 (by lia))
-    have hshift (d : ℕ → ℕ) : ∑ p ∈ range (N + 1), d p * b ^ p =
-        d 0 + b * ∑ p ∈ range N, d (p + 1) * b ^ p := by
-      rw [sum_range_succ', mul_sum]
-      simp only [pow_succ, pow_zero, mul_one]
-      rw [add_comm]
-      congr 1
-      exact sum_congr rfl fun p _ => by ring
-    rw [hshift, hshift] at h
-    have h0 : a 0 = c 0 := by
-      have := congrArg (· % b) h
-      simpa [Nat.add_mul_mod_self_left, Nat.mod_eq_of_lt (ha 0 (by lia)),
-        Nat.mod_eq_of_lt (hc 0 (by lia))] using this
-    rw [h0, Nat.add_left_cancel_iff, Nat.mul_left_cancel_iff hb] at h
-    have ih' := ih (a := fun p => a (p + 1)) (c := fun p => c (p + 1))
-      (fun p hp => ha _ (by lia)) (fun p hp => hc _ (by lia)) h
-    intro p hp
-    rcases p with _ | p
-    · exact h0
-    · exact ih' p (by lia)
+  refine ⟨fun h p hp => ?_, fun h => sum_congr rfl fun p hp => by rw [h p (mem_range.1 hp)]⟩
+  rcases le_or_gt b 1 with hb | hb
+  · have := ha p hp; have := hc p hp; omega
+  · rw [sum_range_mul_pow_eq_ofDigits, sum_range_mul_pow_eq_ofDigits] at h
+    have hL := ofDigits_inj_of_len_eq hb (by simp) (by simpa using ha) (by simpa using hc) h
+    have := congrArg (·[p]?) hL
+    simpa [hp] using this
 
 /-- A number with base-`b` digits below `b` at the positions below `N` is less than `b ^ N`. -/
 theorem sum_range_mul_pow_lt {b N : ℕ} {a : ℕ → ℕ} (ha : ∀ p < N, a p < b) :
     ∑ p ∈ range N, a p * b ^ p < b ^ N := by
-  induction N with
-  | zero => simp
-  | succ N ih =>
-    rw [sum_range_succ, pow_succ]
-    have h₁ := ih fun p hp => ha p (by lia)
-    have h₂ : a N * b ^ N ≤ (b - 1) * b ^ N := Nat.mul_le_mul_right _ (by have := ha N; lia)
-    have h₃ : b ^ N + (b - 1) * b ^ N = b ^ N * b := by
-      obtain ⟨c, rfl⟩ := Nat.exists_eq_add_of_le ((Nat.zero_le _).trans_lt (ha N (by lia)))
-      simp only [Nat.add_sub_cancel_left]
-      ring
-    lia
+  rcases N.eq_zero_or_pos with rfl | hN
+  · simp
+  rcases le_or_gt b 1 with hb | hb
+  · obtain rfl : b = 1 := by have := ha 0 hN; omega
+    simpa using fun i hi => by have := ha i hi; omega
+  · rw [sum_range_mul_pow_eq_ofDigits]
+    simpa using ofDigits_lt_base_pow_length (l := (List.range N).map a) hb (by simpa using ha)
 
 end Nat
 
diff --git a/Complexity/Computability/Kolmogorov/Incompressibility.lean b/Complexity/Computability/Kolmogorov/Incompressibility.lean
index 1132a9df85..a25e4ddf07 100644
--- a/Complexity/Computability/Kolmogorov/Incompressibility.lean
+++ b/Complexity/Computability/Kolmogorov/Incompressibility.lean
@@ -22,8 +22,6 @@ of length `n` have complexity below `n - c` [Li and Vitányi, Chapter 2][LiVitan
 
 ## Main results
 
-* `Cslib.Kolmogorov.encard_setOf_length_lt_add_one`: there are `2 ^ n - 1` binary strings of
-  length below `n`, using `Cslib.BitString.encard_setOf_length_eq` for each exact length.
 * `Cslib.Kolmogorov.DescriptionMethod.encard_setOf_ecomplexity_lt`,
   `Cslib.Kolmogorov.DescriptionMethod.encard_setOf_etimeBoundedComplexity_lt`: fewer than `2 ^ r`
   objects have (time-bounded) complexity below `r`.
@@ -48,24 +46,6 @@ of length `n` have complexity below `n - c` [Li and Vitányi, Chapter 2][LiVitan
 
 namespace Cslib.Kolmogorov
 
-/-! ### Counting binary strings -/
-
-/-- There are `2 ^ n - 1` binary strings of length below `n`. -/
-theorem encard_setOf_length_lt_add_one (n : ℕ) :
-    {p : List Bool | p.length < n}.encard + 1 = 2 ^ n := by
-  induction n with
-  | zero => simp
-  | succ n ih =>
-    have hunion : {p : List Bool | p.length < n + 1} =
-        {p | p.length < n} ∪ {p | p.length = n} := by
-      ext p
-      simp only [Set.mem_ofPred_eq, Set.mem_union]
-      omega
-    have hdisj : Disjoint {p : List Bool | p.length < n} {p | p.length = n} :=
-      Set.disjoint_left.mpr fun _ hlt heq => Nat.ne_of_lt hlt heq
-    rw [hunion, Set.encard_union_eq hdisj, add_right_comm, ih, BitString.encard_setOf_length_eq,
-      pow_succ, mul_two]
-
 namespace DescriptionMethod
 
 variable {α : Type*} (M : DescriptionMethod α)
@@ -85,8 +65,10 @@ theorem encard_setOf_ecomplexity_lt (r : ℕ) : {x | M.ecomplexity x < r}.encard
     Set.encard_le_encard_of_injOn (fun _ hx => (hf hx).1)
       fun _ hx _ hy hxy => (hf hx).2.unique (hxy ▸ (hf hy).2)
   have htop : {p : List Bool | p.length < r}.encard ≠ ⊤ :=
-    ne_top_of_le_ne_top (by simp) (le_self_add.trans_eq (encard_setOf_length_lt_add_one r))
-  rw [← ENat.add_one_le_iff (ne_top_of_le_ne_top htop hle), ← encard_setOf_length_lt_add_one r]
+    ne_top_of_le_ne_top (by simp)
+      (le_self_add.trans_eq (BitString.encard_setOf_length_lt_add_one r))
+  rw [← ENat.add_one_le_iff (ne_top_of_le_ne_top htop hle),
+    ← BitString.encard_setOf_length_lt_add_one r]
   exact add_le_add_left hle 1
 
 /-- Fewer than `2 ^ r` objects have time-bounded complexity below `r`, for every time bound. -/
diff --git a/Complexity/Computability/Kolmogorov/Partrec.lean b/Complexity/Computability/Kolmogorov/Partrec.lean
index d1615238d9..1fdf79df75 100644
--- a/Complexity/Computability/Kolmogorov/Partrec.lean
+++ b/Complexity/Computability/Kolmogorov/Partrec.lean
@@ -9,6 +9,7 @@ module
 
 public import Complexity.Computability.Kolmogorov.Invariance
 public import Complexity.Computability.Kolmogorov.SelfDelimiting
+public import Complexity.Foundations.Data.Nat.Bits
 public import Mathlib.Computability.PartrecCode
 import Mathlib.Computability.Primrec.List
 
@@ -79,15 +80,6 @@ namespace Cslib.Kolmogorov
 
 open Encodable Denumerable Nat.Partrec
 
-/-- Folding `Nat.bit` over a binary string, which inverts `Nat.bits` (`Nat.foldr_bit_bits`), is
-primitive recursive. -/
-theorem _root_.Primrec.list_foldr_nat_bit : Primrec fun l : List Bool => l.foldr Nat.bit 0 := by
-  have hbit : Primrec₂ fun (_ : List Bool) (bn : Bool × ℕ) => Nat.bit bn.1 bn.2 :=
-    Primrec₂.mk <| (Primrec.cond (Primrec.fst.comp Primrec.snd)
-      (Primrec.nat_double_succ.comp (Primrec.snd.comp Primrec.snd))
-      (Primrec.nat_double.comp (Primrec.snd.comp Primrec.snd))).of_eq fun _ => rfl
-  exact (Primrec.list_foldr Primrec.id (Primrec.const 0) hbit).of_eq fun _ => rfl
-
 /-- The decoder of the self-delimiting code is primitive recursive. -/
 theorem primrec_decodeSelfDelimiting : Primrec decodeSelfDelimiting := by
   have hk : Primrec fun q : List Bool => q.idxOf false :=
diff --git a/Complexity/Computability/PCP/DegreeReduction.lean b/Complexity/Computability/PCP/DegreeReduction.lean
index 42f1bc88d9..56a651d4c5 100644
--- a/Complexity/Computability/PCP/DegreeReduction.lean
+++ b/Complexity/Computability/PCP/DegreeReduction.lean
@@ -9,6 +9,7 @@ module
 
 public import Complexity.Computability.PCP.RegularConstraintGraph
 public import Complexity.Foundations.Combinatorics.Expander.Mixing
+import Complexity.Foundations.Data.Finset.Quantile
 
 /-!
 # Degree reduction
@@ -70,22 +71,6 @@ in Dinur's analysis.
 
 open Finset
 
-/-- **Plurality**: some value of a function on a finite type is taken at least as often as any
-other. -/
-private theorem Fintype.exists_forall_card_filter_le_card_filter {ι α : Type*} [Fintype ι]
-    [Nonempty α]
-    [DecidableEq α] (f : ι → α) : ∃ a, ∀ b, #{i | f i = b} ≤ #{i | f i = a} := by
-  rcases isEmpty_or_nonempty ι with h | ⟨⟨i₀⟩⟩
-  · exact ⟨Classical.arbitrary α, fun b ↦ by simp [univ_eq_empty]⟩
-  obtain ⟨i, -, hi⟩ := univ.exists_max_image (fun i ↦ #{j | f j = f i}) ⟨i₀, mem_univ _⟩
-  refine ⟨f i, fun b ↦ ?_⟩
-  by_cases hb : ∃ j, f j = b
-  · obtain ⟨j, rfl⟩ := hb
-    exact hi j (mem_univ _)
-  · simp only [not_exists] at hb
-    rw [filter_false_of_mem fun j _ ↦ hb j, Finset.card_empty]
-    exact Nat.zero_le _
-
 namespace Cslib.PCP
 
 namespace ConstraintGraph
diff --git a/Complexity/Computability/USTCON/Reader/Correct.lean b/Complexity/Computability/USTCON/Reader/Correct.lean
index a424019f91..23f215e111 100644
--- a/Complexity/Computability/USTCON/Reader/Correct.lean
+++ b/Complexity/Computability/USTCON/Reader/Correct.lean
@@ -8,8 +8,7 @@ module
 -- upstream: candidate
 
 public import Complexity.Computability.USTCON.Reader.Defs
-import Mathlib.Data.Nat.Bits
-import Mathlib.Data.Nat.Size
+import Complexity.Foundations.Data.Nat.Bits
 
 /-!
 # Correctness of the read machine for undirected connectivity
@@ -143,14 +142,6 @@ theorem readBit_of_addr_none {q : State} (h : addr q = none) :
 
 /-! ### The header -/
 
-/-- Halving a positive number removes one binary digit. -/
-theorem size_div_two_add_one {n : ℕ} (hn : n ≠ 0) : Nat.size (n / 2) + 1 = Nat.size n := by
-  have hpos := Nat.size_pos.2 (Nat.pos_of_ne_zero hn)
-  rw [← Nat.size_eq_bits_len, ← Nat.size_eq_bits_len, ← Nat.div2_val, Nat.div2_bits_eq_tail,
-    List.length_tail]
-  rw [← Nat.size_eq_bits_len] at hpos
-  omega
-
 /-- The state after the header: the number of vertices, the source and the target are counted,
 and the halvings start from the depth `524` and the walk length `136240`. -/
 def headerState (I : USTCONInstance) : State :=
@@ -215,7 +206,7 @@ private theorem reaches_size (q : State) (m d l : ℕ) :
       · rw [readBit_of_addr_none rfl]
         simp [step, hm.ne']
       · have h := ih (m / 2) (Nat.div_lt_self hm (by norm_num)) (d + 16) (l + 4168)
-        have hs := size_div_two_add_one hm.ne'
+        have hs := Nat.size_div_two_add_one hm.ne'
         have e₁ : d + 16 * Nat.size m = d + 16 + 16 * Nat.size (m / 2) := by rw [← hs]; ring
         have e₂ : l + 4168 * Nat.size m = l + 4168 + 4168 * Nat.size (m / 2) := by
           rw [← hs]; ring
diff --git a/Complexity/Computability/USTCON/Reader/Invariant.lean b/Complexity/Computability/USTCON/Reader/Invariant.lean
index 78805f5b1e..472a4876c4 100644
--- a/Complexity/Computability/USTCON/Reader/Invariant.lean
+++ b/Complexity/Computability/USTCON/Reader/Invariant.lean
@@ -9,7 +9,7 @@ module
 
 public import Complexity.Computability.USTCON.Reader.Correct
 public import Complexity.Computability.USTCON.Reader.Encode
-import Mathlib.Data.Nat.Size
+import Complexity.Foundations.Data.Nat.Bits
 import Complexity.Computability.Machines.Turing.MultiTape.Complexity.LinearSpaceArith
 
 /-!
@@ -179,7 +179,7 @@ private theorem inv_size {m d l : ℕ} (hm : m ≤ I.n) (hd : d + 16 * Nat.size
   · simp only [Nat.size_zero, mul_zero, add_zero] at hd hl
     simp only [step, headerState, init, ite_true]
     exact ⟨by constructor <;> bound_tac, rfl, rfl, rfl, hd, hl⟩
-  · have hsz := size_div_two_add_one hm₀.ne'
+  · have hsz := Nat.size_div_two_add_one hm₀.ne'
     simp only [step, headerState, init, hm₀.ne', ite_false]
     refine ⟨by constructor <;> bound_tac, rfl, ?_, ?_⟩ <;> dsimp only <;> omega
 
diff --git a/Complexity/Foundations/Data/BitString/ShortWords.lean b/Complexity/Foundations/Data/BitString/ShortWords.lean
index 5a465fef1f..7a44328f28 100644
--- a/Complexity/Foundations/Data/BitString/ShortWords.lean
+++ b/Complexity/Foundations/Data/BitString/ShortWords.lean
@@ -31,6 +31,8 @@ leaves some word of length `n` unused.
 ## Main results
 
 * `Cslib.BitString.encard_setOf_length_eq`: there are `2 ^ n` words of length `n`.
+* `Cslib.BitString.encard_setOf_length_lt_add_one`: there are `2 ^ n - 1` words of length below
+  `n`.
 * `Cslib.BitString.exists_length_eq_notMem`: fewer than `2 ^ n` words leave a word of length `n`
   unused.
 * `Cslib.BitString.mem_shortWords`: membership is the length bound.
@@ -50,6 +52,22 @@ theorem encard_setOf_length_eq (n : ℕ) : {p : List Bool | p.length = n}.encard
   rw [ENat.card_eq_coe_fintype_card, card_vector]
   simp
 
+/-- There are `2 ^ n - 1` binary strings of length below `n`. -/
+theorem encard_setOf_length_lt_add_one (n : ℕ) :
+    {p : List Bool | p.length < n}.encard + 1 = 2 ^ n := by
+  induction n with
+  | zero => simp
+  | succ n ih =>
+    have hunion : {p : List Bool | p.length < n + 1} =
+        {p | p.length < n} ∪ {p | p.length = n} := by
+      ext p
+      simp only [Set.mem_ofPred_eq, Set.mem_union]
+      omega
+    have hdisj : Disjoint {p : List Bool | p.length < n} {p | p.length = n} :=
+      Set.disjoint_left.mpr fun _ hlt heq => Nat.ne_of_lt hlt heq
+    rw [hunion, Set.encard_union_eq hdisj, add_right_comm, ih, encard_setOf_length_eq,
+      pow_succ, mul_two]
+
 /-- Fewer than `2 ^ n` words leave a word of length `n` unused. -/
 theorem exists_length_eq_notMem (Q : List (List Bool)) (n : ℕ) (hQ : Q.length < 2 ^ n) :
     ∃ w : List Bool, w.length = n ∧ w ∉ Q := by
diff --git a/Complexity/Foundations/Data/BitString/WordCount.lean b/Complexity/Foundations/Data/BitString/WordCount.lean
index 7a74cd92f8..fdc69b6d59 100644
--- a/Complexity/Foundations/Data/BitString/WordCount.lean
+++ b/Complexity/Foundations/Data/BitString/WordCount.lean
@@ -11,14 +11,18 @@ public import Complexity.Foundations.Data.BitString.List
 public import Complexity.Foundations.Data.BitString.List.Binary
 public import Mathlib.Algebra.BigOperators.Group.Finset.Basic
 public import Mathlib.Data.Fintype.Pi
+public import Mathlib.Data.ZMod.Basic
 public import Mathlib.Order.PiLex
 import Complexity.Foundations.Combinatorics.MajorityVote
 import Mathlib.Algebra.BigOperators.Group.Finset.Piecewise
 import Mathlib.Algebra.BigOperators.Ring.Finset
+import Mathlib.Data.Finset.Sort
 import Mathlib.Data.Fintype.BigOperators
 import Mathlib.Data.Fintype.Prod
 import Mathlib.Data.List.GetD
+import Mathlib.Data.Nat.Choose.Sum
 import Mathlib.Logic.Equiv.Fin.Basic
+import Mathlib.Tactic.Linarith
 import Mathlib.Tactic.Positivity
 import Mathlib.Tactic.Ring
 
@@ -57,6 +61,16 @@ represent sets of words.
 * `Cslib.BitString.card_filter_not_any`, `Cslib.BitString.card_filter_all`: the constant words.
 * `Cslib.BitString.ofFn_decide_lt`: the unary word of `k` bits `true` among `K`.
 * `Cslib.BitString.wordLt_ofFn_iff`: `wordLt` is the lexicographic order.
+* `Cslib.BitString.odd_prod_iff`, `Cslib.BitString.odd_one_add_prod_one_add`: parity of products
+  and the parity form of a disjunction.
+* `Cslib.BitString.card_filter_forall_apply_mem`: counting functions with restricted values on an
+  injective family of points.
+* `Cslib.BitString.two_pow_mul_card_filter_exists_le`: union bound for random strings.
+* `Cslib.BitString.sum_range_neg_two_pow_mul_choose`,
+  `Cslib.BitString.sum_range_neg_two_pow_mul_choose_zmod`: the parity of `c` from binomial
+  coefficients, over `ℤ` and modulo `2 ^ K`.
+* `Cslib.BitString.card_filter_strictMono`, `Cslib.BitString.strictMono_of_lt_succ`: strictly
+  increasing tuples count subsets.
 -/
 
 @[expose] public section
@@ -290,4 +304,158 @@ theorem card_filter_binaryValue_lt {n k : ℕ} (hk : k ≤ 2 ^ n) :
     obtain ⟨w, hw⟩ := exists_binaryValue_eq ((Finset.mem_range.mp hj).trans_le hk)
     exact ⟨w, by simpa [hw] using hj, hw⟩
 
+/-! ### Parity, subsets, and binomial amplification -/
+
+/-- A product of naturals is odd exactly when every factor is. -/
+theorem odd_prod_iff {ι : Type*} {s : Finset ι} (f : ι → ℕ) :
+    Odd (∏ j ∈ s, f j) ↔ ∀ j ∈ s, Odd (f j) := by
+  classical
+  induction s using Finset.induction_on with
+  | empty => simp
+  | insert a s ha ih => rw [Finset.prod_insert ha, Nat.odd_mul, ih, Finset.forall_mem_insert]
+
+/-- **The parity form of a disjunction**: `1 + ∏ⱼ (1 + cⱼ)` is odd exactly when some `cⱼ` is
+odd. -/
+theorem odd_one_add_prod_one_add {ι : Type*} [Fintype ι] (c : ι → ℕ) :
+    Odd (1 + ∏ j, (1 + c j)) ↔ ∃ j, Odd (c j) := by
+  rw [Nat.add_comm, Nat.odd_add_one, odd_prod_iff]
+  simp only [mem_univ, true_imp_iff, not_forall]
+  refine exists_congr fun j => ?_
+  rw [Nat.add_comm, Nat.odd_add_one, not_not]
+
+/-- The functions `s : ι → X` whose values at the `t` distinct points `f i` lie in `F`: `F` is
+chosen at those points and anything elsewhere. -/
+theorem card_filter_forall_apply_mem {ι X : Type*} [Fintype ι] [DecidableEq ι] [Fintype X]
+    [DecidableEq X] {t : ℕ} (f : Fin t → ι) (hf : Function.Injective f) (F : Finset X) :
+    (univ.filter fun s : ι → X => ∀ i, s (f i) ∈ F).card =
+      #F ^ t * Fintype.card X ^ (Fintype.card ι - t) := by
+  classical
+  have h : (univ.filter fun s : ι → X => ∀ i, s (f i) ∈ F) =
+      Fintype.piFinset fun j => if j ∈ Finset.image f univ then F else univ := by
+    ext s
+    simp only [mem_filter, mem_univ, true_and, Fintype.mem_piFinset]
+    constructor
+    · intro hs j
+      split
+      · rename_i hj
+        obtain ⟨i, -, rfl⟩ := Finset.mem_image.1 hj
+        exact hs i
+      · exact mem_univ _
+    · intro hs i
+      have := hs (f i)
+      rwa [ite_eq_left_iff.2 (fun h => absurd (Finset.mem_image_of_mem f (mem_univ i)) h)]
+        at this
+  rw [h, Fintype.card_piFinset]
+  simp only [apply_ite Finset.card, card_univ]
+  rw [Finset.prod_ite, Finset.prod_const, Finset.prod_const]
+  have himg : (univ.filter fun j => j ∈ Finset.image f univ) = Finset.image f univ := by
+    ext j; simp
+  have hcard : #(Finset.image f univ) = t := by
+    rw [Finset.card_image_of_injective _ hf, card_univ, Fintype.card_fin]
+  rw [himg, hcard, Finset.filter_not, himg, Finset.card_sdiff_of_subset (subset_univ _), hcard,
+    card_univ]
+
+/-- **The union bound for random strings**: if each `x` is bad for at most a `2 ^ (-e')` fraction
+of the random strings, some `x` of length `M` is bad for at most a `2 ^ (M - e')` fraction. -/
+theorem two_pow_mul_card_filter_exists_le {R M e' : ℕ}
+    {Bad : (Fin R → Bool) → (Fin M → Bool) → Prop}
+    [∀ r x, Decidable (Bad r x)]
+    (h : ∀ x, 2 ^ e' * (univ.filter fun r => Bad r x).card ≤ 2 ^ R) :
+    2 ^ e' * (univ.filter fun r => ∃ x, Bad r x).card ≤ 2 ^ M * 2 ^ R := by
+  classical
+  have hsub : (univ.filter fun r => ∃ x, Bad r x) ⊆
+      univ.biUnion fun x => univ.filter fun r => Bad r x := by
+    intro r hr
+    simp only [mem_filter, mem_univ, true_and] at hr
+    obtain ⟨x, hx⟩ := hr
+    exact mem_biUnion.2 ⟨x, mem_univ _, by simpa using hx⟩
+  calc 2 ^ e' * (univ.filter fun r => ∃ x, Bad r x).card
+      ≤ 2 ^ e' * ∑ x, (univ.filter fun r => Bad r x).card :=
+        Nat.mul_le_mul_left _ ((card_le_card hsub).trans card_biUnion_le)
+    _ = ∑ x : Fin M → Bool, 2 ^ e' * (univ.filter fun r => Bad r x).card := mul_sum ..
+    _ ≤ ∑ _x : Fin M → Bool, 2 ^ R := sum_le_sum fun x _ => h x
+    _ = 2 ^ M * 2 ^ R := by simp
+
+/-- **The parity of `c` from the binomial expansion of `(1 - 2) ^ c`**:
+`∑ i < c, (-2) ^ i * choose c (i + 1)` is `1` for odd `c` and `0` for even `c`. -/
+theorem sum_range_neg_two_pow_mul_choose (c : ℕ) :
+    ∑ i ∈ range c, (-2 : ℤ) ^ i * (c.choose (i + 1) : ℤ) = if Odd c then 1 else 0 := by
+  have hbin : ∑ i ∈ range (c + 1), (-2 : ℤ) ^ i * (c.choose i : ℤ) = (-1) ^ c := by
+    have := add_pow (-2 : ℤ) 1 c
+    simp only [one_pow, mul_one] at this
+    rw [show (-2 : ℤ) + 1 = -1 by norm_num] at this
+    rw [this]
+  rw [sum_range_succ'] at hbin
+  simp only [pow_zero, Nat.choose_zero_right, Nat.cast_one, mul_one] at hbin
+  have h : -2 * ∑ i ∈ range c, (-2 : ℤ) ^ i * (c.choose (i + 1) : ℤ) = (-1) ^ c - 1 := by
+    rw [mul_sum]
+    rw [← hbin]
+    simp only [pow_succ]
+    ring_nf
+  split
+  · rename_i hc
+    rw [hc.neg_one_pow] at h
+    linarith
+  · rename_i hc
+    rw [(Nat.not_odd_iff_even.1 hc).neg_one_pow, sub_self] at h
+    linarith
+
+/-- **The parity of `c` modulo `2 ^ K`**: only the first `K` binomial terms matter. -/
+theorem sum_range_neg_two_pow_mul_choose_zmod (c K : ℕ) :
+    ∑ i ∈ range K, (-2 : ZMod (2 ^ K)) ^ i * (c.choose (i + 1) : ZMod (2 ^ K)) =
+      if Odd c then 1 else 0 := by
+  have hexact := congrArg (Int.cast : ℤ → ZMod (2 ^ K)) (sum_range_neg_two_pow_mul_choose c)
+  push_cast at hexact
+  rw [← hexact]
+  have hK : (-2 : ZMod (2 ^ K)) ^ K = 0 := by
+    have h2 : (2 : ZMod (2 ^ K)) ^ K = 0 := by
+      exact_mod_cast ZMod.natCast_self (2 ^ K)
+    rw [neg_pow, h2, mul_zero]
+  have h₁ : ∑ i ∈ range (K + c), (-2 : ZMod (2 ^ K)) ^ i * (c.choose (i + 1) : ZMod (2 ^ K)) =
+      ∑ i ∈ range K, (-2 : ZMod (2 ^ K)) ^ i * (c.choose (i + 1) : ZMod (2 ^ K)) := by
+    rw [sum_range_add]
+    simp [pow_add, hK]
+  have h₂ : ∑ i ∈ range (c + K), (-2 : ZMod (2 ^ K)) ^ i * (c.choose (i + 1) : ZMod (2 ^ K)) =
+      ∑ i ∈ range c, (-2 : ZMod (2 ^ K)) ^ i * (c.choose (i + 1) : ZMod (2 ^ K)) := by
+    rw [sum_range_add]
+    simp [Nat.choose_eq_zero_of_lt (by omega : c < c + _ + 1)]
+  rw [← h₁, ← h₂, Nat.add_comm]
+
+/-- **Strictly increasing tuples count subsets**: the strictly increasing `k`-tuples of elements
+of `A` are as many as the `k`-element subsets of `A`. -/
+theorem card_filter_strictMono {β : Type*} [LinearOrder β] [Fintype β] (A : Finset β) (k : ℕ)
+    [DecidablePred fun g : Fin k → β => StrictMono g ∧ ∀ i, g i ∈ A] :
+    (univ.filter fun g : Fin k → β => StrictMono g ∧ ∀ i, g i ∈ A).card = (#A).choose k := by
+  classical
+  rw [← card_powersetCard]
+  refine card_bij (fun g _ => univ.image g) ?_ ?_ ?_
+  · intro g hg
+    simp only [mem_filter, mem_univ, true_and] at hg
+    rw [mem_powersetCard]
+    refine ⟨fun x hx => ?_, ?_⟩
+    · obtain ⟨i, -, rfl⟩ := mem_image.1 hx
+      exact hg.2 i
+    · rw [card_image_of_injective _ hg.1.injective, card_univ, Fintype.card_fin]
+  · intro g hg g' hg' h
+    simp only [mem_filter, mem_univ, true_and] at hg hg'
+    have hc : (univ.image g).card = k := by
+      rw [card_image_of_injective _ hg.1.injective, card_univ, Fintype.card_fin]
+    have h1 : g = (univ.image g).orderEmbOfFin hc :=
+      orderEmbOfFin_unique hc (fun i => mem_image_of_mem g (mem_univ i)) hg.1
+    have h2 : g' = (univ.image g).orderEmbOfFin hc :=
+      orderEmbOfFin_unique hc (fun i => h ▸ mem_image_of_mem g' (mem_univ i)) hg'.1
+    rw [h1, ← h2]
+  · intro s hs
+    rw [mem_powersetCard] at hs
+    refine ⟨s.orderEmbOfFin hs.2, ?_, image_orderEmbOfFin_univ s hs.2⟩
+    simp only [mem_filter, mem_univ, true_and]
+    exact ⟨(s.orderEmbOfFin hs.2).strictMono, fun i => hs.1 (orderEmbOfFin_mem s hs.2 i)⟩
+
+/-- A tuple increasing at every step is strictly increasing. -/
+theorem strictMono_of_lt_succ {β : Type*} [Preorder β] {k : ℕ} {g : Fin k → β}
+    (h : ∀ (i : ℕ) (hi : i + 1 < k), g ⟨i, by omega⟩ < g ⟨i + 1, hi⟩) : StrictMono g := by
+  cases k with
+  | zero => exact fun i => i.elim0
+  | succ k => exact Fin.strictMono_iff_lt_succ.2 fun i => h i (by omega)
+
 end Cslib.BitString
diff --git a/Complexity/Foundations/Data/Finset/Quantile.lean b/Complexity/Foundations/Data/Finset/Quantile.lean
index 3c0e5b0fb2..2b1d0a66e6 100644
--- a/Complexity/Foundations/Data/Finset/Quantile.lean
+++ b/Complexity/Foundations/Data/Finset/Quantile.lean
@@ -10,6 +10,7 @@ module
 public import Complexity.Init
 public import Mathlib.Basic.Real.Basic
 public import Mathlib.Data.Finset.Card
+public import Mathlib.Data.Fintype.Basic
 import Mathlib.Data.Finset.Max
 import Mathlib.Tactic.Linarith
 
@@ -24,6 +25,8 @@ belong to both level sets; no injectivity or tie-breaking assumption is required
 
 * `Finset.exists_quantile`: select a pivot retaining the requested proportions on both sides.
 * `Finset.exists_median`: select a median pivot with at least half of the elements on each side.
+* `Fintype.exists_forall_card_filter_le_card_filter`: some value of a function on a finite type is
+  taken at least as often as any other.
 
 ## References
 
@@ -87,4 +90,19 @@ theorem exists_median (s : Finset α) (hs : s.Nonempty) (score : α → β) :
   · exact_mod_cast
       (by linarith : (s.card : ℝ) ≤ 2 * ((s.filter fun x => score p ≤ score x).card : ℝ))
 
+/-- **Plurality**: some value of a function on a finite type is taken at least as often as any
+other. -/
+theorem _root_.Fintype.exists_forall_card_filter_le_card_filter {ι α : Type*} [Fintype ι]
+    [Nonempty α] [DecidableEq α] (f : ι → α) : ∃ a, ∀ b, #{i | f i = b} ≤ #{i | f i = a} := by
+  rcases isEmpty_or_nonempty ι with h | ⟨⟨i₀⟩⟩
+  · exact ⟨Classical.arbitrary α, fun b ↦ by simp [univ_eq_empty]⟩
+  obtain ⟨i, -, hi⟩ := univ.exists_max_image (fun i ↦ #{j | f j = f i}) ⟨i₀, mem_univ _⟩
+  refine ⟨f i, fun b ↦ ?_⟩
+  by_cases hb : ∃ j, f j = b
+  · obtain ⟨j, rfl⟩ := hb
+    exact hi j (mem_univ _)
+  · simp only [not_exists] at hb
+    rw [filter_false_of_mem fun j _ ↦ hb j, Finset.card_empty]
+    exact Nat.zero_le _
+
 end Finset
diff --git a/Complexity/Foundations/Data/Nat/Bits.lean b/Complexity/Foundations/Data/Nat/Bits.lean
index 8b3a2e42f5..bced8b2bee 100644
--- a/Complexity/Foundations/Data/Nat/Bits.lean
+++ b/Complexity/Foundations/Data/Nat/Bits.lean
@@ -9,9 +9,10 @@ module
 
 public import Complexity.Init
 public import Mathlib.Algebra.BigOperators.Fin
+public import Mathlib.Computability.Primrec.List
 public import Mathlib.Data.Nat.Bits
+public import Mathlib.Data.Nat.Size
 import Mathlib.Data.List.OfFn
-import Mathlib.Data.Nat.Size
 
 /-!
 # Recovering a natural number from its binary digits
@@ -24,6 +25,8 @@ with initial value zero reconstructs the original number.
 * `Nat.foldr_bit_bits`: folding `Nat.bit` over the binary representation of `n` gives `n`.
 * `Nat.foldr_bit_lt`, `Nat.foldr_bit_testBit`: fixed-width little-endian reconstruction.
 * `Nat.foldr_bit_ofFn`: reconstruction is the sum of the digits' binary place values.
+* `Nat.size_div_two_add_one`: halving a positive number removes one binary digit.
+* `Primrec.list_foldr_nat_bit`: folding `Nat.bit` over a binary string is primitive recursive.
 -/
 
 @[expose] public section
@@ -71,3 +74,20 @@ theorem Nat.foldr_bit_testBit {n K : ℕ} (h : n.size ≤ K) :
     rw [List.range_succ_eq_map, List.map_cons, List.map_map, List.foldr_cons]
     have hmap : n.testBit ∘ Nat.succ = (n / 2).testBit := funext fun i => Nat.testBit_succ n i
     rw [hmap, ih hn, ← Nat.shiftRight_one, Nat.bit_testBit_zero_shiftRight_one]
+
+/-- Halving a positive number removes one binary digit. -/
+theorem Nat.size_div_two_add_one {n : ℕ} (hn : n ≠ 0) : Nat.size (n / 2) + 1 = Nat.size n := by
+  have hpos := Nat.size_pos.2 (Nat.pos_of_ne_zero hn)
+  rw [← Nat.size_eq_bits_len, ← Nat.size_eq_bits_len, ← Nat.div2_val, Nat.div2_bits_eq_tail,
+    List.length_tail]
+  rw [← Nat.size_eq_bits_len] at hpos
+  omega
+
+/-- Folding `Nat.bit` over a binary string, which inverts `Nat.bits` (`Nat.foldr_bit_bits`), is
+primitive recursive. -/
+theorem Primrec.list_foldr_nat_bit : Primrec fun l : List Bool => l.foldr Nat.bit 0 := by
+  have hbit : Primrec₂ fun (_ : List Bool) (bn : Bool × ℕ) => Nat.bit bn.1 bn.2 :=
+    Primrec₂.mk <| (Primrec.cond (Primrec.fst.comp Primrec.snd)
+      (Primrec.nat_double_succ.comp (Primrec.snd.comp Primrec.snd))
+      (Primrec.nat_double.comp (Primrec.snd.comp Primrec.snd))).of_eq fun _ => rfl
+  exact (Primrec.list_foldr Primrec.id (Primrec.const 0) hbit).of_eq fun _ => rfl

From 75702850688c9fafcded1e7a9feb705dbfe10ead Mon Sep 17 00:00:00 2001
From: Samuel Schlesinger <samschlesinger@google.com>
Date: Sat, 24 Oct 2026 07:35:10 +0000
Subject: [PATCH 2/2] refactor(foundations): split Primrec.list_foldr_nat_bit
 into Nat/Primrec (#610)

---
 Complexity.lean                               |  1 +
 .../Computability/Kolmogorov/Partrec.lean     |  2 +-
 Complexity/Foundations/Data/Nat/Bits.lean     | 11 -------
 Complexity/Foundations/Data/Nat/Primrec.lean  | 30 +++++++++++++++++++
 4 files changed, 32 insertions(+), 12 deletions(-)
 create mode 100644 Complexity/Foundations/Data/Nat/Primrec.lean

diff --git a/Complexity.lean b/Complexity.lean
index c7a64783db..5d5a7a2116 100644
--- a/Complexity.lean
+++ b/Complexity.lean
@@ -1700,6 +1700,7 @@ public import Complexity.Foundations.Data.Nat.Log
 public import Complexity.Foundations.Data.Nat.PolynomialBound.Closure
 public import Complexity.Foundations.Data.Nat.PolynomialBound.Exponential
 public import Complexity.Foundations.Data.Nat.PolynomialBound.Log
+public import Complexity.Foundations.Data.Nat.Primrec
 public import Complexity.Foundations.Data.Nat.Radix
 public import Complexity.Foundations.Data.OrderedSet
 public import Complexity.Foundations.Data.Polynomial.CoeffList
diff --git a/Complexity/Computability/Kolmogorov/Partrec.lean b/Complexity/Computability/Kolmogorov/Partrec.lean
index 1fdf79df75..d1e1ca1dcc 100644
--- a/Complexity/Computability/Kolmogorov/Partrec.lean
+++ b/Complexity/Computability/Kolmogorov/Partrec.lean
@@ -9,7 +9,7 @@ module
 
 public import Complexity.Computability.Kolmogorov.Invariance
 public import Complexity.Computability.Kolmogorov.SelfDelimiting
-public import Complexity.Foundations.Data.Nat.Bits
+public import Complexity.Foundations.Data.Nat.Primrec
 public import Mathlib.Computability.PartrecCode
 import Mathlib.Computability.Primrec.List
 
diff --git a/Complexity/Foundations/Data/Nat/Bits.lean b/Complexity/Foundations/Data/Nat/Bits.lean
index bced8b2bee..14dc3c4f04 100644
--- a/Complexity/Foundations/Data/Nat/Bits.lean
+++ b/Complexity/Foundations/Data/Nat/Bits.lean
@@ -9,7 +9,6 @@ module
 
 public import Complexity.Init
 public import Mathlib.Algebra.BigOperators.Fin
-public import Mathlib.Computability.Primrec.List
 public import Mathlib.Data.Nat.Bits
 public import Mathlib.Data.Nat.Size
 import Mathlib.Data.List.OfFn
@@ -26,7 +25,6 @@ with initial value zero reconstructs the original number.
 * `Nat.foldr_bit_lt`, `Nat.foldr_bit_testBit`: fixed-width little-endian reconstruction.
 * `Nat.foldr_bit_ofFn`: reconstruction is the sum of the digits' binary place values.
 * `Nat.size_div_two_add_one`: halving a positive number removes one binary digit.
-* `Primrec.list_foldr_nat_bit`: folding `Nat.bit` over a binary string is primitive recursive.
 -/
 
 @[expose] public section
@@ -82,12 +80,3 @@ theorem Nat.size_div_two_add_one {n : ℕ} (hn : n ≠ 0) : Nat.size (n / 2) + 1
     List.length_tail]
   rw [← Nat.size_eq_bits_len] at hpos
   omega
-
-/-- Folding `Nat.bit` over a binary string, which inverts `Nat.bits` (`Nat.foldr_bit_bits`), is
-primitive recursive. -/
-theorem Primrec.list_foldr_nat_bit : Primrec fun l : List Bool => l.foldr Nat.bit 0 := by
-  have hbit : Primrec₂ fun (_ : List Bool) (bn : Bool × ℕ) => Nat.bit bn.1 bn.2 :=
-    Primrec₂.mk <| (Primrec.cond (Primrec.fst.comp Primrec.snd)
-      (Primrec.nat_double_succ.comp (Primrec.snd.comp Primrec.snd))
-      (Primrec.nat_double.comp (Primrec.snd.comp Primrec.snd))).of_eq fun _ => rfl
-  exact (Primrec.list_foldr Primrec.id (Primrec.const 0) hbit).of_eq fun _ => rfl
diff --git a/Complexity/Foundations/Data/Nat/Primrec.lean b/Complexity/Foundations/Data/Nat/Primrec.lean
new file mode 100644
index 0000000000..30b2feb428
--- /dev/null
+++ b/Complexity/Foundations/Data/Nat/Primrec.lean
@@ -0,0 +1,30 @@
+/-
+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 (Mathlib, `Mathlib/Computability/Primrec/List.lean`)
+
+public import Complexity.Foundations.Data.Nat.Bits
+public import Mathlib.Computability.Primrec.List
+
+/-!
+# Primitive recursiveness of binary-digit reconstruction
+
+## Main results
+
+* `Primrec.list_foldr_nat_bit`: folding `Nat.bit` over a binary string is primitive recursive.
+-/
+
+@[expose] public section
+
+/-- Folding `Nat.bit` over a binary string, which inverts `Nat.bits` (`Nat.foldr_bit_bits`), is
+primitive recursive. -/
+theorem Primrec.list_foldr_nat_bit : Primrec fun l : List Bool => l.foldr Nat.bit 0 := by
+  have hbit : Primrec₂ fun (_ : List Bool) (bn : Bool × ℕ) => Nat.bit bn.1 bn.2 :=
+    Primrec₂.mk <| (Primrec.cond (Primrec.fst.comp Primrec.snd)
+      (Primrec.nat_double_succ.comp (Primrec.snd.comp Primrec.snd))
+      (Primrec.nat_double.comp (Primrec.snd.comp Primrec.snd))).of_eq fun _ => rfl
+  exact (Primrec.list_foldr Primrec.id (Primrec.const 0) hbit).of_eq fun _ => rfl