diff --git a/Complexity/Computability/Complexity/FineGrained/SparseBranchAsymptotics.lean b/Complexity/Computability/Complexity/FineGrained/SparseBranchAsymptotics.lean
index 2c22eecd4..0e15b561f 100644
--- a/Complexity/Computability/Complexity/FineGrained/SparseBranchAsymptotics.lean
+++ b/Complexity/Computability/Complexity/FineGrained/SparseBranchAsymptotics.lean
@@ -9,6 +9,7 @@ module
 
 public import Complexity.Init
 public import Complexity.Computability.Complexity.FineGrained.SparseParitySchedule
+import Complexity.Foundations.Data.Nat.Log
 import Mathlib.Analysis.Complex.ExponentialBounds
 
 /-!
@@ -92,7 +93,6 @@ public section
 namespace Cslib.Complexity.SubexponentialSAT.ReplacementParams
 
 open Cslib.Complexity.SubexponentialSAT
-open Cslib.Logic.PL (clog_two_le_two_mul_of_le_two_mul)
 
 /-! ### 1. Free-variable (`n / 2 ≤ n' ≤ n`) to original-variable (`n`) `rowCost` transfer -/
 
@@ -118,7 +118,7 @@ theorem Feasible.mul_rowCost_le_of_le_two_mul {β n n' b_occ w_width M' : ℕ}
   have hsqrt_le : Real.sqrt (Nat.clog 2 n) ≤ 2 * Real.sqrt (Nat.clog 2 n') := by
     have hclog_le : (Nat.clog 2 n : ℝ) ≤ (2 : ℝ) ^ 2 * (Nat.clog 2 n' : ℝ) := by
       have hnat : Nat.clog 2 n ≤ 2 * Nat.clog 2 n' :=
-        clog_two_le_two_mul_of_le_two_mul hn_le (by omega)
+        Nat.clog_two_le_two_mul_of_le_two_mul hn_le (by omega)
       have hcast : (Nat.clog 2 n : ℝ) ≤ 2 * (Nat.clog 2 n' : ℝ) := by exact_mod_cast hnat
       have hnn : (0 : ℝ) ≤ (Nat.clog 2 n' : ℝ) := Nat.cast_nonneg _
       linarith
diff --git a/Complexity/Computability/Complexity/FineGrained/SparseParitySchedule.lean b/Complexity/Computability/Complexity/FineGrained/SparseParitySchedule.lean
index 5f276f8f8..0f78918b9 100644
--- a/Complexity/Computability/Complexity/FineGrained/SparseParitySchedule.lean
+++ b/Complexity/Computability/Complexity/FineGrained/SparseParitySchedule.lean
@@ -10,6 +10,7 @@ module
 public import Complexity.Init
 public import Complexity.Computability.Complexity.FineGrained.SparseBranchSchedule
 public import Complexity.Logics.Propositional.CNF.SparseParityCounter
+import Complexity.Foundations.Data.Nat.Log
 
 /-!
 # Section 6.3 compiled CNF parity-row schedule feasibility and domain-examination bounds
@@ -433,19 +434,6 @@ theorem CNF.exists_greedy_parityRowSystem_branch_schedule {β : ℕ} (hβ : 1 
 
 /-! ### 4. Unconditional polylogarithmic schedule discharge for `B ≤ C_B * (Nat.clog 2 n) ^ β_B` -/
 
-/-- When `n ≤ 2 * n'` and `2 ≤ n'`, `Nat.clog 2 n ≤ 2 * Nat.clog 2 n'`. -/
-theorem clog_two_le_two_mul_of_le_two_mul {n n' : ℕ} (hn : n ≤ 2 * n') (hn' : 2 ≤ n') :
-    Nat.clog 2 n ≤ 2 * Nat.clog 2 n' := by
-  have h1 : 1 ≤ Nat.clog 2 n' :=
-    (Nat.lt_clog_iff_pow_lt one_lt_two).mpr (by omega : 2 ^ 0 < n')
-  have h2 : n ≤ 2 ^ (Nat.clog 2 n' + 1) := by
-    calc n ≤ 2 * n' := hn
-      _ ≤ 2 * 2 ^ Nat.clog 2 n' := Nat.mul_le_mul_left 2 (Nat.le_pow_clog one_lt_two n')
-      _ = 2 ^ (Nat.clog 2 n' + 1) := (pow_succ' 2 _).symm
-  have h3 : Nat.clog 2 n ≤ Nat.clog 2 n' + 1 :=
-    (Nat.clog_le_iff_le_pow one_lt_two).mpr h2
-  omega
-
 /-- Coefficient for the polynomial bound on `initialRowWeightBound B m` when
 `B ≤ C_B * (Nat.clog 2 n) ^ β_B` and `m ≤ B * n`. -/
 def CNF.initialRowWeightCoeff (C_B β_B : ℕ) : ℕ :=
@@ -546,7 +534,7 @@ private theorem parityBranchThreshold_succ_and_width_le_clog_pow {n n' m B W k C
           ring
   have hlam_pow : lam ^ (2 * β_B + 4) ≤ 2 ^ (2 * β_B + 4) * lam' ^ (2 * β_B + 4) := by
     calc lam ^ (2 * β_B + 4) ≤ (2 * lam') ^ (2 * β_B + 4) :=
-          Nat.pow_le_pow_left (clog_two_le_two_mul_of_le_two_mul hn_le hn') _
+          Nat.pow_le_pow_left (Nat.clog_two_le_two_mul_of_le_two_mul hn_le hn') _
       _ = 2 ^ (2 * β_B + 4) * lam' ^ (2 * β_B + 4) := mul_pow 2 lam' _
   have hthresh_lam' :
       CNF.parityBranchThreshold k W n + 1 ≤ Nat.clog 2 n' ^ (2 * β_B + 5) := by
diff --git a/Complexity/Computability/Complexity/Problems/SAT/ExactOne/DrawingAssembly.lean b/Complexity/Computability/Complexity/Problems/SAT/ExactOne/DrawingAssembly.lean
index 82041ec91..12b0576d1 100644
--- a/Complexity/Computability/Complexity/Problems/SAT/ExactOne/DrawingAssembly.lean
+++ b/Complexity/Computability/Complexity/Problems/SAT/ExactOne/DrawingAssembly.lean
@@ -10,6 +10,7 @@ module
 public import Complexity.Computability.Complexity.Problems.SAT.ExactOne.DrawingData
 public import Complexity.Computability.Complexity.Problems.SAT.ExactOne.DrawingCounts
 public import Complexity.Computability.Complexity.Problems.SAT.ExactOne.DrawingClauseVertices
+import Complexity.Foundations.Data.List.Lookup
 import Mathlib.Data.List.GetD
 
 /-!
@@ -67,7 +68,7 @@ private theorem placed_occurrence_routes (pcs : List PositivePlacedClause)
     rfl
   change pc.1.zipIdx.map (fun x => (pcs.getD i ([], (0, 0), [])).2.2.getD x.2 []) = _
   rw [hg]
-  exact map_getD_zipIdx pc.1 pc.2.2 [] (hc pc (List.mem_of_getElem? hi'))
+  exact List.map_getD_zipIdx pc.1 pc.2.2 [] (hc pc (List.mem_of_getElem? hi'))
 
 /-- The occurrence-indexed view has exactly the compiler's actual position and route lists. -/
 theorem positiveFormulaDrawing_drawing (φ : CNF ℕ) (d : Graph.OrthogonalDrawing) :
diff --git a/Complexity/Computability/Complexity/Problems/SAT/ExactOne/DrawingClauseVertices.lean b/Complexity/Computability/Complexity/Problems/SAT/ExactOne/DrawingClauseVertices.lean
index 2c21a8e38..0cbfa3849 100644
--- a/Complexity/Computability/Complexity/Problems/SAT/ExactOne/DrawingClauseVertices.lean
+++ b/Complexity/Computability/Complexity/Problems/SAT/ExactOne/DrawingClauseVertices.lean
@@ -8,6 +8,7 @@ module
 -- upstream: candidate
 
 public import Complexity.Computability.Complexity.Problems.SAT.ExactOne.DrawingVertexBoxes
+import Complexity.Foundations.Data.List.Lookup
 import Mathlib.Data.List.GetD
 import Mathlib.Data.List.Nodup
 
@@ -43,16 +44,6 @@ theorem clauseGeometry_clause_length (φ : CNF ℕ) (d : Graph.OrthogonalDrawing
   simpa only [clauseGeometry, collaredPrefixGeometry, profilePrefixGeometry,
     LocalGeometry.toPrefix, List.length_map] using profileGeometry_clause_length (clauseProfile c)
 
-/-- Mapping `ys.getD a.2 fallback` over `xs.zipIdx` recovers `ys` when `ys.length = xs.length`. -/
-theorem map_getD_zipIdx {A B : Type*} (xs : List A) (ys : List B) (fallback : B)
-    (hlen : ys.length = xs.length) :
-    (xs.zipIdx.map fun a => ys.getD a.2 fallback) = ys := by
-  apply List.ext_getElem
-  · simpa using hlen.symm
-  · intro i hi hj
-    simp only [List.getElem_map, List.getElem_zipIdx, Nat.zero_add]
-    rw [List.getD_eq_getElem _ _ hj]
-
 /-- A clause block lists precisely the translated local clause positions in order. -/
 theorem positiveClauseBlock_positions (φ : CNF ℕ) (d : Graph.OrthogonalDrawing)
     (i : ℕ) (c : Clause ℕ) :
@@ -60,7 +51,7 @@ theorem positiveClauseBlock_positions (φ : CNF ℕ) (d : Graph.OrthogonalDrawin
       (clauseGeometry φ d i c).clausePositions.map (positiveBoxOrigin φ d i + ·) := by
   simp only [positiveClauseBlock, List.map_map, Function.comp_def]
   have he := congrArg (List.map (positiveBoxOrigin φ d i + ·))
-    (map_getD_zipIdx (profileFormula (clauseProfile c))
+    (List.map_getD_zipIdx (profileFormula (clauseProfile c))
       (clauseGeometry φ d i c).clausePositions (0, 0) (clauseGeometry_clause_length φ d i c))
   simpa only [List.map_map, Function.comp_def, LocalGeometry.clausePosition] using he
 
diff --git a/Complexity/Computability/Interactive/Plain.lean b/Complexity/Computability/Interactive/Plain.lean
index 98b59cf37..5dd69a5b9 100644
--- a/Complexity/Computability/Interactive/Plain.lean
+++ b/Complexity/Computability/Interactive/Plain.lean
@@ -142,12 +142,6 @@ private theorem runLaw_output {s : Spec} {StmtIn StmtOut : Type}
   · exact e.elim
   · rfl
 
-/-- A uniform upper bound on `(f a).toOuterMeasure t` bounds `(p.bind f).toOuterMeasure t`. -/
-theorem toOuterMeasure_bind_le {α β : Type} (p : PMF α) (f : α → PMF β) (t : Set β)
-    {K : ℝ≥0∞} (h : ∀ a, (f a).toOuterMeasure t ≤ K) : (p.bind f).toOuterMeasure t ≤ K := by
-  rw [PMF.toOuterMeasure_bind_apply]
-  exact Probability.PMF.tsum_mul_le_of_forall_le _ h
-
 private theorem toOuterMeasure_bind_pure {α β : Type} (p : PMF α) (g : α → β) (t : Set β) :
     (p.bind fun a => PMF.pure (g a)).toOuterMeasure t = p.toOuterMeasure (g ⁻¹' t) := by
   rw [← PMF.toOuterMeasure_map_apply]
@@ -176,7 +170,7 @@ private theorem rbrFrom_le : ∀ (s : Spec) (smp : PerChallenge ProbComp s)
     simp [runStrategy, hw]
   | .prover M I :: s, smp, ε, S, wins, h, hS, _, st => by
     simp only [runStrategy, plainLaw_bind]
-    refine toOuterMeasure_bind_le _ _ _ fun p => ?_
+    refine Probability.PMF.toOuterMeasure_bind_le _ _ _ fun p => ?_
     rcases p with ⟨msg, st'⟩
     simp only [plainLaw_pure]
     rw [toOuterMeasure_bind_pure]
@@ -195,7 +189,7 @@ private theorem rbrFrom_le : ∀ (s : Spec) (smp : PerChallenge ProbComp s)
         rw [Set.indicator_of_mem hc]
         exact Probability.PMF.toOuterMeasure_le_one _ _
       · rw [Set.indicator_of_notMem hc, zero_add]
-        refine toOuterMeasure_bind_le _ _ _ fun st' => ?_
+        refine Probability.PMF.toOuterMeasure_bind_le _ _ _ fun st' => ?_
         simp only [plainLaw_pure]
         rw [toOuterMeasure_bind_pure]
         exact rbrFrom_le s smp.2 ε.2 (fun p => S (some (c, p))) (fun τ => wins (c, τ)) (h.2 c) hc
@@ -220,7 +214,7 @@ theorem Verifier.RbrSound.sound {s : Spec} {StmtIn StmtOut : Type}
   obtain ⟨S, hinit, hround⟩ := h
   intro x hx α P
   rw [World.plain_eval_execute, PMF.toOuterMeasure_map_apply, plainLaw_bind]
-  exact toOuterMeasure_bind_le _ _ _ fun st => rbrFrom_le s V.samplers ε (S x) _ (hround x)
-    (hinit x hx) st
+  exact Probability.PMF.toOuterMeasure_bind_le _ _ _ fun st =>
+    rbrFrom_le s V.samplers ε (S x) _ (hround x) (hinit x hx) st
 
 end Cslib.Interactive
diff --git a/Complexity/Computability/Interactive/Sequential.lean b/Complexity/Computability/Interactive/Sequential.lean
index fcee3df09..e37fa6ffd 100644
--- a/Complexity/Computability/Interactive/Sequential.lean
+++ b/Complexity/Computability/Interactive/Sequential.lean
@@ -716,7 +716,7 @@ theorem Verifier.KnowledgeSound.append {V₁ : Verifier OracleSpec.empty s₁ S
     congr 1
     ext r₂
     cases hout : V₁.outputOn x r₁.1 <;> simp [T₁, Spec.Transcript.split_append, hout]
-  · refine toOuterMeasure_bind_le _ _ _ fun r₁ => ?_
+  · refine Probability.PMF.toOuterMeasure_bind_le _ _ _ fun r₁ => ?_
     rw [PMF.toOuterMeasure_map_apply]
     cases hout : V₁.outputOn x r₁.1 with
     | none =>
diff --git a/Complexity/Computability/Machines/Turing/MultiTape/Encodings/Length.lean b/Complexity/Computability/Machines/Turing/MultiTape/Encodings/Length.lean
index a52f94c47..838e28335 100644
--- a/Complexity/Computability/Machines/Turing/MultiTape/Encodings/Length.lean
+++ b/Complexity/Computability/Machines/Turing/MultiTape/Encodings/Length.lean
@@ -23,6 +23,8 @@ certificate, in terms of the input.
 * `Turing.MultiTapeTM.length_encList`: the exact length.
 * `Turing.MultiTapeTM.sum_length_le_length_encList`: the encoded elements are no longer, in total,
   than the encoded list.
+* `Turing.MultiTapeTM.length_unframe_add_dropFrame_le`: the unframed prefix and remaining suffix
+  of any bit list satisfy `2 * (unframe v).length + (dropFrame v).length ≤ v.length`.
 -/
 
 @[expose] public section
@@ -50,4 +52,15 @@ theorem sum_length_le_length_encList (l : List α) :
   | nil => simp
   | cons a l ih => simp only [List.map_cons, List.sum_cons]; omega
 
+/-- The unframed prefix and remaining suffix of any bit list satisfy
+`2 * (unframe v).length + (dropFrame v).length ≤ v.length`. -/
+theorem length_unframe_add_dropFrame_le :
+    ∀ v : List Bool, 2 * (unframe v).length + (dropFrame v).length ≤ v.length
+  | [] | [true] => by simp [unframe, dropFrame]
+  | false :: v => by simp [unframe, dropFrame]
+  | true :: b :: v => by
+    have ih := length_unframe_add_dropFrame_le v
+    simp only [unframe, dropFrame, List.length_cons]
+    omega
+
 end Turing.MultiTapeTM
diff --git a/Complexity/Computability/Machines/Turing/MultiTape/Internal/PolyTimeLoops.lean b/Complexity/Computability/Machines/Turing/MultiTape/Internal/PolyTimeLoops.lean
index 3ea9e5d98..d73ac2314 100644
--- a/Complexity/Computability/Machines/Turing/MultiTape/Internal/PolyTimeLoops.lean
+++ b/Complexity/Computability/Machines/Turing/MultiTape/Internal/PolyTimeLoops.lean
@@ -31,16 +31,6 @@ private theorem unaryWordCertificate {α : Type} {input : α ↪ List Bool} {cou
     ComputableInPolyTime (fun x => List.replicate (count x) true) input encBits := by
   exact h.of_enc_eq fun _ => rfl
 
-private theorem foldlCapture {π β α : Type} (par : π) (step : π → β → α → β)
-    (list : List α) (init : β) :
-    list.foldl (fun state value => (state.1, step state.1 state.2 value)) (par, init) =
-      (par, list.foldl (step par) init) := by
-  induction list generalizing init with
-  | nil => rfl
-  | cons a list ih =>
-    simp only [List.foldl_cons]
-    exact ih (step par init a)
-
 namespace ComputableInPolyTime
 
 /-- A unary-output certificate bounds the actual numeric value by a polynomial in input size. -/
@@ -49,6 +39,12 @@ theorem polyBounded {α : Type*} {input : α ↪ List Bool} {f : α → ℕ}
     PolyBounded (fun x => (input x).length) f := by
   simpa only [encUnary_apply, List.length_replicate] using hf.polyBounded_length
 
+/-- A unary-output polynomial-time function is polynomially bounded in its unary input. -/
+theorem polynomiallyBounded {f : ℕ → ℕ} (hf : ComputableInPolyTime f encUnary encUnary) :
+    PolynomiallyBounded f :=
+  (show PolyBounded (fun n : ℕ => n) f by
+    simpa only [encUnary_apply, List.length_replicate] using hf.polyBounded).polynomiallyBounded
+
 
 /-- A polynomial bound on the encoded accumulators of reachable prefixes suffices for a
 uniform polynomial-time fold. The list and callback encodings are preserved. -/
@@ -136,12 +132,12 @@ theorem foldlWith {γ α β π : Type} {encIn : γ ↪ List Bool} {encA : α ↪
     (step := fun state value => (state.1, step state.1 state.2 value))
     hlist hstart hjoint (B := C) (PolyBounded.of_forall_le c d hC) (by
       intro x i hi
-      simp only [foldlCapture, length_encPair]
+      simp only [List.foldl_keep_fst, length_encPair]
       dsimp [C]
       exact Nat.add_le_add_left (hstates x i hi) _)
   have hsecond : ComputableInPolyTime (fun p : π × β => p.2) (encPair encP encB) encB :=
     ComputableInPolyTime.snd encP encB
-  simpa only [Function.comp_def, foldlCapture] using ComputableInPolyTime.comp hsecond hfold
+  simpa only [Function.comp_def, List.foldl_keep_fst] using ComputableInPolyTime.comp hsecond hfold
 
 /-- A computed captured parameter and a unary loop count give a uniform loop when every
 reachable iterate has polynomially bounded encoded size. -/
diff --git a/Complexity/Computability/PolyTime/BooleanAnalysis/BoundedIncidenceCounter.lean b/Complexity/Computability/PolyTime/BooleanAnalysis/BoundedIncidenceCounter.lean
index ad972a107..74b832c13 100644
--- a/Complexity/Computability/PolyTime/BooleanAnalysis/BoundedIncidenceCounter.lean
+++ b/Complexity/Computability/PolyTime/BooleanAnalysis/BoundedIncidenceCounter.lean
@@ -24,6 +24,7 @@ import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Na
 import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Nat.BinaryDiv
 import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Plain
 import Complexity.Computability.Machines.Turing.MultiTape.Encodings.List.Size
+import Complexity.Foundations.Data.List.Fold
 import Mathlib.Data.List.GetD
 import Mathlib.Tactic.Linarith
 import Mathlib.Tactic.Positivity
@@ -472,7 +473,7 @@ private theorem exists_computableInO_signedMeasJet :
         (evalMeasPayload (Cslib.Radix.measurementValues dc.2.2.1.1 dc.2.2.1.2 i, pa.1)).elim pa.2
           fun y => addJet pa.1.2.1.1 pa.1.2.1.2.1 pa.2 y) := by
       funext pa i; cases evalMeasPayload _ <;> rfl
-    rw [hfn]; exact foldl_keep_fst
+    rw [hfn]; exact List.foldl_keep_fst
       (fun (m : MeasStepCtx) (acc : JetRows) (i : ℕ) =>
         (evalMeasPayload (Cslib.Radix.measurementValues dc.2.2.1.1 dc.2.2.1.2 i, m)).elim acc
           (fun y => addJet m.2.1.1 m.2.1.2.1 acc y))
@@ -683,7 +684,7 @@ private theorem exists_computableInO_nodeJet :
       (eSubAcc (SubsetPairFold.runPrefix subsetPairStepBody qs.2.1.1 qs.1 j
         (qs.2, zeroJet qs.2.2.2.1.1 qs.2.2.2.1.2.1)).2.2).length ≤ B_sub qs := by
     intro qs j hj; rw [SubsetPairFold.runPrefix_acc]; simp only [subsetPairStepBody_eq]
-    rw [foldl_keep_fst (fun (s : SubsetStepCtx) (acc : JetRows) (i : ℕ) =>
+    rw [List.foldl_keep_fst (fun (s : SubsetStepCtx) (acc : JetRows) (i : ℕ) =>
       addJet s.2.2.1.1 s.2.2.1.2.1 acc
         (evalSignedMeasJet (SubsetPairFold.unrankSubsetPair qs.2.1.1 qs.1 i, s)))]
     have hf_le := length_encJetRows_foldl_optAddJet_le (J := qs.2.2.2.1.1) (ℓ := qs.2.2.2.1.2.1)
@@ -731,7 +732,7 @@ private theorem exists_computableInO_nodeJet :
         (Nat.mul_le_mul_left co (Nat.pow_le_pow_left (Nat.add_le_add_right hinp_len 1) do_))
       have hfst_eq : inp.2.1 = qs.2 := by
         dsimp only [inp]; rw [SubsetPairFold.runPrefix_acc]; simp only [subsetPairStepBody_eq]
-        rw [foldl_keep_fst (fun (s : SubsetStepCtx) (acc : JetRows) (i : ℕ) =>
+        rw [List.foldl_keep_fst (fun (s : SubsetStepCtx) (acc : JetRows) (i : ℕ) =>
           addJet s.2.2.1.1 s.2.2.1.2.1 acc
             (evalSignedMeasJet (SubsetPairFold.unrankSubsetPair qs.2.1.1 qs.1 i, s)))]
       have hdc_len : (eDC (inp.1, inp.2.1)).length ≤ L_dc qs := by
diff --git a/Complexity/Computability/PolyTime/CommonCountingAccum.lean b/Complexity/Computability/PolyTime/CommonCountingAccum.lean
index 722899fb5..44da4746d 100644
--- a/Complexity/Computability/PolyTime/CommonCountingAccum.lean
+++ b/Complexity/Computability/PolyTime/CommonCountingAccum.lean
@@ -17,6 +17,7 @@ import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Fo
 import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.List
 import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Plain
 import Complexity.Computability.Machines.Turing.MultiTape.Encodings.List.Size
+import Complexity.Foundations.Data.List.Fold
 import Complexity.Foundations.Data.List.OfFn
 import Mathlib.Algebra.BigOperators.Ring.Finset
 import Mathlib.Algebra.Order.BigOperators.Group.List
@@ -451,14 +452,6 @@ theorem jetL1Norm_weightedProdJet_le (J ℓ : ℕ) (w : ℤ) (groups : List JetR
 
 section SharedHelpers
 
-theorem foldl_keep_fst {ι π α : Type*} (step : π → α → ι → α)
-    (par : π) (xs : List ι) (init : α) :
-    xs.foldl (fun pa i => (pa.1, step pa.1 pa.2 i)) (par, init) =
-      (par, xs.foldl (step par) init) := by
-  induction xs generalizing init with
-  | nil => rfl
-  | cons _ _ ih => exact ih _
-
 private def rangeAddJet (J ℓ j : ℕ) (f : ℕ → JetRows) : JetRows :=
   (List.range j).foldl (fun acc i => addJet J ℓ acc (f i)) (zeroJet J ℓ)
 private theorem isTableShape_rangeAddJet (J ℓ j : ℕ) (f : ℕ → JetRows) :
@@ -742,7 +735,7 @@ private theorem streamGroupJetSumRunPrefix_snd_snd_foldl (J ℓ d j : ℕ) (ctx
     (BooleanFold.runPrefix (groupSumBody evalGroupProd) d j (((J, ℓ), ctx), zeroJet J ℓ)).2.2 =
       (((J, ℓ), ctx), rangeAddJet J ℓ j fun i => evalGroupProd (ctx, (d, lowBits d i))) :=
   (BooleanFold.prefix_accumulator (groupSumBody evalGroupProd) d j _).trans
-    (foldl_keep_fst (fun (par : (ℕ × ℕ) × α) acc i =>
+    (List.foldl_keep_fst (fun (par : (ℕ × ℕ) × α) acc i =>
       addJet par.1.1 par.1.2 acc (evalGroupProd (par.2, (d, lowBits d i))))
       ((J, ℓ), ctx) (List.range j) (zeroJet J ℓ))
 theorem streamGroupJetSumPrefix_eq_foldl (J ℓ d j : ℕ) (ctx : α) :
@@ -757,7 +750,7 @@ theorem toJetTable_streamGroupJetSum_eq_sum (J ℓ d : ℕ) (ctx : α) :
       (enumList d).foldl (fun acc w => addJet J ℓ acc (evalGroupProd (ctx, (d, w))))
         (zeroJet J ℓ) :=
     congrArg Prod.snd ((BooleanFold.run_accumulator (groupSumBody evalGroupProd) d _).trans
-      (foldl_keep_fst (fun (par : (ℕ × ℕ) × α) acc w =>
+      (List.foldl_keep_fst (fun (par : (ℕ × ℕ) × α) acc w =>
         addJet par.1.1 par.1.2 acc (evalGroupProd (par.2, (d, w))))
         ((J, ℓ), ctx) (enumList d) (zeroJet J ℓ)))
   rw [hfold, toJetTable_foldl_addJet, toJetTable_zeroJet, zero_add, enumList, List.map_map,
@@ -976,7 +969,7 @@ private theorem streamOuterJetAccumRunPrefix_snd_foldl (J ℓ j : ℕ) (ctx : α
       (((J, ℓ), ctx), rangeAddJet J ℓ j fun idx =>
         weightedProdJet J ℓ (evalRound (ctx, idx)).1 (evalRound (ctx, idx)).2) :=
   (IndexFold.run_accumulator (outerAccumBody evalRound) j _).trans
-    (foldl_keep_fst (fun (par : (ℕ × ℕ) × α) acc idx =>
+    (List.foldl_keep_fst (fun (par : (ℕ × ℕ) × α) acc idx =>
       combineOuterRound par.1.1 par.1.2 acc (evalRound (par.2, idx)))
       ((J, ℓ), ctx) (List.range j) (zeroJet J ℓ))
 theorem streamOuterJetAccumPrefix_eq_foldl (J ℓ j : ℕ) (ctx : α) :
diff --git a/Complexity/Crypto/Computational/Homomorphic/FixedKey/PolyTime.lean b/Complexity/Crypto/Computational/Homomorphic/FixedKey/PolyTime.lean
index 00332d25c..2251c7da8 100644
--- a/Complexity/Crypto/Computational/Homomorphic/FixedKey/PolyTime.lean
+++ b/Complexity/Crypto/Computational/Homomorphic/FixedKey/PolyTime.lean
@@ -174,9 +174,7 @@ theorem polynomiallyBounded_widths :
       (fun c : Σ m, Circuit Boolean.signature m 1 => (c.1, c.2.code))
       (Boolean.encCircuit 1) (encPair encUnary Boolean.encCode) := .of_eq fun _ => rfl
   have htotal : PolynomiallyBounded (fun n => secretWidth n + ciphertextWidth n) :=
-    (show PolyBounded (fun n : ℕ => n) (fun n => secretWidth n + ciphertextWidth n) by
-      simpa only [encUnary_apply, List.length_replicate, Function.comp_def] using
-        (hview.fst'.comp hD).polyBounded_length).polynomiallyBounded
+    (hview.fst'.comp hD).polynomiallyBounded
   exact ⟨htotal.mono_of_le (fun n => Nat.le_add_right (secretWidth n) (ciphertextWidth n)),
     htotal.mono_of_le (fun n => Nat.le_add_left (ciphertextWidth n) (secretWidth n))⟩
 
@@ -189,11 +187,7 @@ theorem polynomiallyBounded_decryptionSize :
       (Boolean.encCircuit 1) (encPair encUnary Boolean.encCode) := .of_eq fun _ => rfl
   have hlen : ComputableInPolyTime (fun n => (D.circuit n).code.1.length) encUnary encUnary :=
     (ComputableInPolyTime.length_list Boolean.encGate).comp (hview.snd'.fst'.comp hD)
-  have hlength : PolynomiallyBounded (fun n => (D.circuit n).code.1.length) :=
-    (show PolyBounded (fun n : ℕ => n) (fun n => (D.circuit n).code.1.length) by
-      simpa only [encUnary_apply, List.length_replicate] using
-        hlen.polyBounded_length).polynomiallyBounded
-  exact hlength.mono_of_le (fun n => (Circuit.length_code_fst (D.circuit n)).ge)
+  exact hlen.polynomiallyBounded.mono_of_le (fun n => (Circuit.length_code_fst (D.circuit n)).ge)
 
 include hkeyGen hencrypt in
 /-- The constructed scheme's actual key generator is strict PPT. -/
diff --git a/Complexity/Crypto/Computational/Homomorphic/GSW/DepthParameters.lean b/Complexity/Crypto/Computational/Homomorphic/GSW/DepthParameters.lean
index 8475f58e4..fe21eb0f6 100644
--- a/Complexity/Crypto/Computational/Homomorphic/GSW/DepthParameters.lean
+++ b/Complexity/Crypto/Computational/Homomorphic/GSW/DepthParameters.lean
@@ -224,25 +224,23 @@ theorem computableInPolyTime_modulus :
     ComputableInPolyTime modulus encUnary encNat :=
   binary_pow' (const 2) DepthParameters.computableInPolyTime_width
 
-open Parameters (polynomiallyBounded_of_unary)
-
 /-- All unary parameters have polynomial bounds; the modulus is deliberately excluded. -/
 theorem polynomiallyBounded_parameters :
     PolynomiallyBounded dimension ∧ PolynomiallyBounded noise ∧ PolynomiallyBounded width ∧
       PolynomiallyBounded rows ∧ PolynomiallyBounded samples ∧ PolynomiallyBounded depthBudget :=
-  ⟨polynomiallyBounded_of_unary Parameters.computableInPolyTime_dimension,
-    polynomiallyBounded_of_unary Parameters.computableInPolyTime_noise,
-    polynomiallyBounded_of_unary DepthParameters.computableInPolyTime_width,
-    polynomiallyBounded_of_unary DepthParameters.computableInPolyTime_rows,
-    polynomiallyBounded_of_unary DepthParameters.computableInPolyTime_samples,
-    polynomiallyBounded_of_unary computableInPolyTime_depthBudget⟩
+  ⟨Parameters.computableInPolyTime_dimension.polynomiallyBounded,
+    Parameters.computableInPolyTime_noise.polynomiallyBounded,
+    DepthParameters.computableInPolyTime_width.polynomiallyBounded,
+    DepthParameters.computableInPolyTime_rows.polynomiallyBounded,
+    DepthParameters.computableInPolyTime_samples.polynomiallyBounded,
+    computableInPolyTime_depthBudget.polynomiallyBounded⟩
 
 /-- The actual shared-public-matrix error bound is negligible for this new family. -/
 theorem negligible_statistical_error :
     Negligible (fun security => (rows security : ℝ≥0) *
       NNReal.sqrt ((2 : ℝ≥0) ^ rows security / 2 ^ samples security)) :=
   negligible_mul_sqrt_pow_two_div_pow_two
-    (polynomiallyBounded_of_unary DepthParameters.computableInPolyTime_rows)
+    DepthParameters.computableInPolyTime_rows.polynomiallyBounded
     (Filter.Eventually.of_forall entropy_margin)
 
 end Cslib.Crypto.Homomorphic.GSW.DepthParameters
diff --git a/Complexity/Crypto/Computational/Homomorphic/GSW/Parameters.lean b/Complexity/Crypto/Computational/Homomorphic/GSW/Parameters.lean
index 01be9d226..1b5fa407c 100644
--- a/Complexity/Crypto/Computational/Homomorphic/GSW/Parameters.lean
+++ b/Complexity/Crypto/Computational/Homomorphic/GSW/Parameters.lean
@@ -194,30 +194,22 @@ theorem computableInPolyTime_modulus :
   rw [hmodulus]
   fun_prop
 
-/-- Any function computable in polynomial time with unary input and unary output is polynomially
-bounded. -/
-theorem polynomiallyBounded_of_unary {f : ℕ → ℕ}
-    (hf : ComputableInPolyTime f encUnary encUnary) : PolynomiallyBounded f :=
-  (show PolyBounded (fun n : ℕ => n) f by
-    simpa only [encUnary_apply, List.length_replicate] using
-      hf.polyBounded_length).polynomiallyBounded
-
 /-- Every numerical parameter, including the modulus, is polynomially bounded. -/
 theorem polynomiallyBounded_parameters :
     PolynomiallyBounded dimension ∧ PolynomiallyBounded noise ∧ PolynomiallyBounded width ∧
       PolynomiallyBounded rows ∧ PolynomiallyBounded samples ∧ PolynomiallyBounded modulus :=
-  ⟨polynomiallyBounded_of_unary computableInPolyTime_dimension,
-    polynomiallyBounded_of_unary computableInPolyTime_noise,
-    polynomiallyBounded_of_unary computableInPolyTime_width,
-    polynomiallyBounded_of_unary computableInPolyTime_rows,
-    polynomiallyBounded_of_unary computableInPolyTime_samples,
-    polynomiallyBounded_of_unary computableInPolyTime_modulus⟩
+  ⟨computableInPolyTime_dimension.polynomiallyBounded,
+    computableInPolyTime_noise.polynomiallyBounded,
+    computableInPolyTime_width.polynomiallyBounded,
+    computableInPolyTime_rows.polynomiallyBounded,
+    computableInPolyTime_samples.polynomiallyBounded,
+    computableInPolyTime_modulus.polynomiallyBounded⟩
 
 /-- The exact shared-public-matrix error bound is negligible for this positive-noise family. -/
 theorem negligible_statistical_error :
     Negligible (fun security => (rows security : ℝ≥0) *
       NNReal.sqrt ((2 : ℝ≥0) ^ rows security / 2 ^ samples security)) :=
-  negligible_mul_sqrt_pow_two_div_pow_two (polynomiallyBounded_of_unary computableInPolyTime_rows)
+  negligible_mul_sqrt_pow_two_div_pow_two computableInPolyTime_rows.polynomiallyBounded
     (Filter.Eventually.of_forall entropy_margin)
 
 end Cslib.Crypto.Homomorphic.GSW.Parameters
diff --git a/Complexity/Crypto/Computational/Homomorphic/GSW/Security.lean b/Complexity/Crypto/Computational/Homomorphic/GSW/Security.lean
index bdb7baf0b..0a2274447 100644
--- a/Complexity/Crypto/Computational/Homomorphic/GSW/Security.lean
+++ b/Complexity/Crypto/Computational/Homomorphic/GSW/Security.lean
@@ -144,14 +144,8 @@ theorem indCPA_of_decisionLWE {n m w η : ℕ → ℕ}
   have hsource := hLWE (lweDistinguisher n m w adversary)
     (isPPT_lweDistinguisher hn hm hw hadversary)
   have hrows : PolynomiallyBounded (fun k => (n k + 1) * w k) := by
-    have : PolynomiallyBounded n :=
-      (show PolyBounded (fun k : ℕ => k) n by
-        simpa only [encUnary_apply, List.length_replicate] using
-          hn.polyBounded_length).polynomiallyBounded
-    have : PolynomiallyBounded w :=
-      (show PolyBounded (fun k : ℕ => k) w by
-        simpa only [encUnary_apply, List.length_replicate] using
-          hw.polyBounded_length).polynomiallyBounded
+    have : PolynomiallyBounded n := hn.polynomiallyBounded
+    have : PolynomiallyBounded w := hw.polynomiallyBounded
     fun_prop
   have herror := negligible_mul_sqrt_pow_two_div_pow_two hrows hmargin
   apply negligible_of_le
diff --git a/Complexity/Crypto/Computational/Homomorphic/KeyChain/Security.lean b/Complexity/Crypto/Computational/Homomorphic/KeyChain/Security.lean
index e187509fe..189c67656 100644
--- a/Complexity/Crypto/Computational/Homomorphic/KeyChain/Security.lean
+++ b/Complexity/Crypto/Computational/Homomorphic/KeyChain/Security.lean
@@ -68,14 +68,8 @@ theorem negligible_publicKeyChainHybrid {E : Scheme}
     exact (Nat.le_add_left _ _).trans h
   have hred := isPPT_linkAdversary hkeyGen hencrypt htest hdepth hcapacity
   have hpoly : PolynomiallyBounded (fun n => dyadicSize (depth n) * dyadicSize (capacity n)) := by
-    have hd : PolynomiallyBounded depth :=
-      (show PolyBounded (fun n : ℕ => n) depth by
-        simpa only [encUnary_apply, List.length_replicate] using
-          hdepth.polyBounded_length).polynomiallyBounded
-    have hc : PolynomiallyBounded capacity :=
-      (show PolyBounded (fun n : ℕ => n) capacity by
-        simpa only [encUnary_apply, List.length_replicate] using
-          hcapacity.polyBounded_length).polynomiallyBounded
+    have hd : PolynomiallyBounded depth := hdepth.polynomiallyBounded
+    have hc : PolynomiallyBounded capacity := hcapacity.polynomiallyBounded
     fun_prop
   have hneg := (hsecure _ hred).polynomiallyBounded_mul hpoly
   refine negligible_of_le hneg (fun n => ?_)
diff --git a/Complexity/Crypto/Computational/Homomorphic/Leveled/Compactness.lean b/Complexity/Crypto/Computational/Homomorphic/Leveled/Compactness.lean
index bd3b6d803..5bf978879 100644
--- a/Complexity/Crypto/Computational/Homomorphic/Leveled/Compactness.lean
+++ b/Complexity/Crypto/Computational/Homomorphic/Leveled/Compactness.lean
@@ -206,11 +206,8 @@ theorem exists_uniform_decrypt_circuits
     have hlen_unary : ComputableInPolyTime (fun n => (circuits n).code.1.length)
         encUnary encUnary :=
       (ComputableInPolyTime.length_list Boolean.encGate).comp hcode.fst'
-    have hlength : PolynomiallyBounded (fun n => (circuits n).code.1.length) :=
-      (show PolyBounded (fun n : ℕ => n) (fun n => (circuits n).code.1.length) by
-        simpa only [encUnary_apply, List.length_replicate] using
-          hlen_unary.polyBounded_length).polynomiallyBounded
-    exact hlength.mono_of_le fun n => (Circuit.length_code_fst (circuits n)).ge
+    exact hlen_unary.polynomiallyBounded.mono_of_le
+      fun n => (Circuit.length_code_fst (circuits n)).ge
   refine ⟨circuits, hgen, hsize, ?_⟩
   intro budget n sk ciphertext hsk hciphertext
   have hwlen : (sk ++ ciphertext).length = W n := by simp [W, K, hsk, hciphertext]
diff --git a/Complexity/Crypto/Computational/Homomorphic/Leveled/PolyTime.lean b/Complexity/Crypto/Computational/Homomorphic/Leveled/PolyTime.lean
index d6597bb4c..0159efd0e 100644
--- a/Complexity/Crypto/Computational/Homomorphic/Leveled/PolyTime.lean
+++ b/Complexity/Crypto/Computational/Homomorphic/Leveled/PolyTime.lean
@@ -230,13 +230,8 @@ theorem polynomiallyBounded_widths :
   have hview : ComputableInPolyTime
       (fun c : Σ m, Circuit Boolean.signature m 1 => (c.1, c.2.code))
       (Boolean.encCircuit 1) (encPair encUnary Boolean.encCode) := .of_eq fun _ => rfl
-  have htotal_unary : ComputableInPolyTime
-      (fun n => secretWidth n + ciphertextWidth n) encUnary encUnary :=
-    hview.fst'.comp hD
   have htotal : PolynomiallyBounded (fun n => secretWidth n + ciphertextWidth n) :=
-    (show PolyBounded (fun n : ℕ => n) (fun n => secretWidth n + ciphertextWidth n) by
-      simpa only [encUnary_apply, List.length_replicate] using
-        htotal_unary.polyBounded_length).polynomiallyBounded
+    (hview.fst'.comp hD).polynomiallyBounded
   have hsecret : PolynomiallyBounded secretWidth :=
     htotal.mono_of_le (fun n => Nat.le_add_right (secretWidth n) (ciphertextWidth n))
   have hciphertext : PolynomiallyBounded ciphertextWidth :=
diff --git a/Complexity/Crypto/Computational/MAC.lean b/Complexity/Crypto/Computational/MAC.lean
index dbb2976bb..894f92bc0 100644
--- a/Complexity/Crypto/Computational/MAC.lean
+++ b/Complexity/Crypto/Computational/MAC.lean
@@ -1660,17 +1660,6 @@ private theorem computableTidilyInPolyTime_decide_nodup {γ : Type} {encIn : γ
   exact ComputableTidilyInPolyTime.allWithInput (test := fun a x => (list a).count x == 1)
     hlist (by polytime)
 
-/-- The unframed prefix and remaining suffix of any bit list satisfy
-`2 * (unframe v).length + (dropFrame v).length ≤ v.length`. -/
-theorem length_unframe_add_dropFrame_le :
-    ∀ v : List Bool, 2 * (unframe v).length + (dropFrame v).length ≤ v.length
-  | [] | [true] => by simp [unframe, dropFrame]
-  | false :: v => by simp [unframe, dropFrame]
-  | true :: b :: v => by
-    have ih := length_unframe_add_dropFrame_le v
-    simp only [unframe, dropFrame, List.length_cons]
-    omega
-
 namespace NonceMACScheme
 
 attribute [program_certificate]
diff --git a/Complexity/Crypto/Computational/NaorReingold/PRF.lean b/Complexity/Crypto/Computational/NaorReingold/PRF.lean
index bf39cd22b..fd3bf4138 100644
--- a/Complexity/Crypto/Computational/NaorReingold/PRF.lean
+++ b/Complexity/Crypto/Computational/NaorReingold/PRF.lean
@@ -433,7 +433,7 @@ private theorem advantage_evalNaorReingoldTape_uniform_le (inLen outLen : ℕ 
     rw [PMF.bind_comm (Cslib.BitString.uniformList H) ν]
     congr 1; funext α₀
     rw [PMF.bind_comm (Cslib.BitString.uniformList H)
-      (PMF.uniformOfFintype (Fin m → ZMod (F.order d))), ← iid_uniformOfFintype m]
+      (PMF.uniformOfFintype (Fin m → ZMod (F.order d))), ← PMF.iid_uniformOfFintype m]
   change Game.advantage
     ((Cslib.BitString.uniformList (E + (m * E + H))).bind _)
     (F.naorReingoldHashedRealGame _ _ _ _ _ n) ≤ _
diff --git a/Complexity/Crypto/Computational/NaorReingold/Security.lean b/Complexity/Crypto/Computational/NaorReingold/Security.lean
index 9c2efb6b5..24958d108 100644
--- a/Complexity/Crypto/Computational/NaorReingold/Security.lean
+++ b/Complexity/Crypto/Computational/NaorReingold/Security.lean
@@ -927,16 +927,8 @@ private theorem eval_sampleNaorReingoldPair_eq_iid (F : PrimeOrderGroupFamily) (
 
 private theorem pi_uniformOfFintype {ι α : Type*} [Fintype ι] [DecidableEq ι] [Fintype α]
     [Nonempty α] :
-    PMF.pi (fun _ : ι => PMF.uniformOfFintype α) = PMF.uniformOfFintype (ι → α) := by
-  ext f
-  simp only [PMF.pi_apply, PMF.uniformOfFintype_apply, Finset.prod_const, Finset.card_univ,
-    Fintype.card_fun, Nat.cast_pow, ENNReal.inv_pow]
-
-/-- The `k`-fold independent product of `PMF.uniformOfFintype α` is
-`PMF.uniformOfFintype (Fin k → α)`. -/
-theorem iid_uniformOfFintype {α : Type*} [Fintype α] [Nonempty α] (k : ℕ) :
-    PMF.iid (PMF.uniformOfFintype α) k = PMF.uniformOfFintype (Fin k → α) := by
-  rw [PMF.iid_eq_pi, pi_uniformOfFintype]
+    PMF.pi (fun _ : ι => PMF.uniformOfFintype α) = PMF.uniformOfFintype (ι → α) :=
+  PMF.pi_uniformOfFintype (ι := ι) (α := fun _ => α)
 
 private theorem pi_ddhFixedURerandomizeLaw_eq_multi (F : PrimeOrderGroupFamily) (d : F.Desc)
     (ι : Type*) [Fintype ι] [DecidableEq ι] (u₀ v₀ w₀ : F.Carrier d) :
diff --git a/Complexity/Foundations/Data/List/Fold.lean b/Complexity/Foundations/Data/List/Fold.lean
index cd1f5a6d9..2a7447159 100644
--- a/Complexity/Foundations/Data/List/Fold.lean
+++ b/Complexity/Foundations/Data/List/Fold.lean
@@ -16,6 +16,8 @@ public import Mathlib.Data.List.Basic
 ## Main results
 
 * `List.foldl_take_invariant`: an index-dependent invariant holds after every prefix of a fold.
+* `List.foldl_keep_fst`: folding a step that keeps the first component of a pair preserves that
+  component and folds over the second.
 * `List.foldr_ite_eq_of_mem`: a chain of equality tests selects the branch of a contained tag,
   regardless of duplicates or fallback. Used by finite-control certificates.
 
@@ -43,6 +45,16 @@ theorem List.foldl_take_invariant {α β : Type*} (l : List α) (step : β → 
     simpa only [List.take_succ_eq_append_getElem hlt, List.foldl_append,
       List.foldl_cons, List.foldl_nil] using hstep i hlt _ (ih (Nat.le_of_lt hlt))
 
+/-- Folding a step that keeps the first component of a pair preserves that component and folds
+over the second. -/
+theorem List.foldl_keep_fst {ι π α : Type*} (step : π → α → ι → α)
+    (par : π) (xs : List ι) (init : α) :
+    xs.foldl (fun pa i => (pa.1, step pa.1 pa.2 i)) (par, init) =
+      (par, xs.foldl (step par) init) := by
+  induction xs generalizing init with
+  | nil => rfl
+  | cons _ _ ih => exact ih _
+
 /-- A chain of equality tests selects a contained tag, regardless of duplicates or fallback. -/
 theorem List.foldr_ite_eq_of_mem {Tag Value : Type*} [DecidableEq Tag]
     (tags : List Tag) (tag : Tag) (branch : Tag → Value) (fallback : Value) (h : tag ∈ tags) :
diff --git a/Complexity/Foundations/Data/List/Lookup.lean b/Complexity/Foundations/Data/List/Lookup.lean
index 2d1072861..f2c393806 100644
--- a/Complexity/Foundations/Data/List/Lookup.lean
+++ b/Complexity/Foundations/Data/List/Lookup.lean
@@ -32,6 +32,8 @@ import Mathlib.Data.List.OfFn
   updates and bound defaulted reads of numeric register files.
 * `List.getD_map_range`: read a function tabulated over a bounded range.
 * `List.map_range_eq_ofFn`: runtime tabulation agrees with the finite coordinate view.
+* `List.map_getD_zipIdx`: mapping `ys.getD a.2 fallback` over `xs.zipIdx` recovers `ys` when
+  `ys.length = xs.length`.
 * `List.find?_range_getD_eq_sInf`: the least index below `m` passing a test, or `m`, as a search
   over a range.
 -/
@@ -127,6 +129,16 @@ theorem List.map_range_eq_ofFn {α : Type*} (n : ℕ) (f : ℕ → α) :
   intro i hi hi'
   simp
 
+/-- Mapping `ys.getD a.2 fallback` over `xs.zipIdx` recovers `ys` when `ys.length = xs.length`. -/
+theorem List.map_getD_zipIdx {α β : Type*} (xs : List α) (ys : List β) (fallback : β)
+    (hlen : ys.length = xs.length) :
+    (xs.zipIdx.map fun a => ys.getD a.2 fallback) = ys := by
+  apply List.ext_getElem
+  · simpa using hlen.symm
+  · intro i hi hj
+    simp only [List.getElem_map, List.getElem_zipIdx, Nat.zero_add]
+    rw [List.getD_eq_getElem _ _ hj]
+
 /-- The least index below `m` passing a test, or `m`, as a search over `List.range m`. -/
 theorem List.find?_range_getD_eq_sInf (m : ℕ) (p : ℕ → Bool) :
     ((List.range m).find? p).getD m = sInf {i | i = m ∨ p i = true} := by
diff --git a/Complexity/Foundations/Data/Nat/Log.lean b/Complexity/Foundations/Data/Nat/Log.lean
index 2cbe61571..e3387cc1f 100644
--- a/Complexity/Foundations/Data/Nat/Log.lean
+++ b/Complexity/Foundations/Data/Nat/Log.lean
@@ -29,6 +29,8 @@ stays polynomial after logarithmically many rounds. Similarly `2 ^ (⌊log₂ n
 * `Nat.two_pow_clog_two_le`: `2 ^ ⌈log₂ n⌉ ≤ 2 (n + 1)`, also for `n = 0`.
 * `Nat.log_add_one_le`: `⌊log_b (n + 1)⌋ ≤ ⌊log_b n⌋ + 1`.
 * `Nat.mul_log_le_add_sq`: `m * ⌊log_b n⌋ ≤ n + m * m` for `1 < b`.
+* `Nat.clog_two_le_two_mul_of_le_two_mul`: `⌈log₂ n⌉ ≤ 2 * ⌈log₂ n'⌉` when `n ≤ 2 * n'` and
+  `2 ≤ n'`.
 -/
 
 @[expose] public section
@@ -96,4 +98,15 @@ theorem mul_log_le_add_sq (hb : 1 < b) (m n : ℕ) : m * log b n ≤ n + m * m :
       rw [← Nat.mul_add, Nat.sub_add_cancel h.le]
     omega
 
+/-- When `n ≤ 2 * n'` and `2 ≤ n'`, `⌈log₂ n⌉ ≤ 2 * ⌈log₂ n'⌉`. -/
+theorem clog_two_le_two_mul_of_le_two_mul {n n' : ℕ} (hn : n ≤ 2 * n') (hn' : 2 ≤ n') :
+    clog 2 n ≤ 2 * clog 2 n' := by
+  have h1 : 1 ≤ clog 2 n' := (lt_clog_iff_pow_lt Nat.one_lt_two).mpr (by omega : 2 ^ 0 < n')
+  have h2 : n ≤ 2 ^ (clog 2 n' + 1) :=
+    calc n ≤ 2 * n' := hn
+      _ ≤ 2 * 2 ^ clog 2 n' := Nat.mul_le_mul_left 2 (le_pow_clog Nat.one_lt_two n')
+      _ = 2 ^ (clog 2 n' + 1) := Nat.pow_succ'.symm
+  have h3 : clog 2 n ≤ clog 2 n' + 1 := (clog_le_iff_le_pow Nat.one_lt_two).mpr h2
+  omega
+
 end Nat
diff --git a/Complexity/Probability/IID.lean b/Complexity/Probability/IID.lean
index 74388f5b5..5aaa16af5 100644
--- a/Complexity/Probability/IID.lean
+++ b/Complexity/Probability/IID.lean
@@ -39,7 +39,8 @@ bounds.
 
 * `Cslib.Probability.PMF.iid_apply`, `Cslib.Probability.PMF.mem_support_iid_iff`: masses and
   support.
-* `Cslib.Probability.PMF.iid_map`, `Cslib.Probability.PMF.iid_eq_pi`: images and finite products.
+* `Cslib.Probability.PMF.iid_map`, `Cslib.Probability.PMF.iid_eq_pi`,
+  `Cslib.Probability.PMF.iid_uniformOfFintype`: images, finite products, and uniform tuples.
 * `Cslib.Probability.PMF.iid_card_ge_le`: the majority tail bound.
 
 ## References
@@ -110,6 +111,11 @@ theorem iid_eq_pi [Finite α] (μ : PMF α) (k : ℕ) : iid μ k = pi (fun _ : F
   ext v
   rw [iid_apply, pi_apply]
 
+/-- Independent uniform draws on a nonempty finite type form the uniform distribution on tuples. -/
+theorem iid_uniformOfFintype [Fintype α] [Nonempty α] (k : ℕ) :
+    iid (PMF.uniformOfFintype α) k = PMF.uniformOfFintype (Fin k → α) := by
+  rw [iid_eq_pi, pi_uniformOfFintype]
+
 /-- If `0 ≤ a ≤ b`, `r ≤ t` and `t + u = 2 r`, then `a ^ t b ^ u ≤ (a b) ^ r`. -/
 private theorem pow_mul_pow_le {a b : ℝ} (ha : 0 ≤ a) (hab : a ≤ b) {r t u : ℕ} (ht : r ≤ t)
     (htu : t + u = 2 * r) : a ^ t * b ^ u ≤ (a * b) ^ r := by
diff --git a/Complexity/Probability/PMF/Event.lean b/Complexity/Probability/PMF/Event.lean
index ce673d7ce..0b2a00749 100644
--- a/Complexity/Probability/PMF/Event.lean
+++ b/Complexity/Probability/PMF/Event.lean
@@ -8,6 +8,7 @@ module
 -- upstream: candidate (addition to `Cslib/Probability/PMF.lean`)
 
 public import Complexity.Probability.PMF
+import Complexity.Probability.PMF.Bind
 
 /-!
 # Event probabilities of discrete distributions
@@ -39,7 +40,8 @@ masses of `true` and `false` under a Boolean distribution sum to one
   `Cslib.Probability.PMF.toOuterMeasure_toReal_pos_iff`: real-valued event probabilities.
 * `Cslib.Probability.PMF.filter_apply_toReal`: conditioned masses.
 * `Cslib.Probability.PMF.toOuterMeasure_bind_toReal`: averaging over a first stage.
-* `Cslib.Probability.PMF.toOuterMeasure_bind_failure_le`,
+* `Cslib.Probability.PMF.toOuterMeasure_bind_le`,
+  `Cslib.Probability.PMF.toOuterMeasure_bind_failure_le`,
   `Cslib.Probability.PMF.toOuterMeasure_bind_failure_toReal_le`,
   `Cslib.Probability.PMF.toOuterMeasure_bind_ge_mul`: composing failure and success bounds.
 * `Cslib.Probability.PMF.toOuterMeasure_rate_ge`: average bias as the probability of good inputs.
@@ -144,6 +146,14 @@ theorem toOuterMeasure_bind_toReal [Fintype α] (p : PMF α) (kernel : α → PM
     (fun a _ => ENNReal.mul_ne_top (PMF.apply_ne_top _ _) (toOuterMeasure_ne_top _ _))]
   simp only [ENNReal.toReal_mul]
 
+/-- A uniform upper bound on `(kernel a).toOuterMeasure event` bounds
+`(p.bind kernel).toOuterMeasure event`. -/
+theorem toOuterMeasure_bind_le (p : PMF α) (kernel : α → PMF β) (event : Set β)
+    {error : ENNReal} (h : ∀ a, (kernel a).toOuterMeasure event ≤ error) :
+    (p.bind kernel).toOuterMeasure event ≤ error := by
+  rw [PMF.toOuterMeasure_bind_apply]
+  exact tsum_mul_le_of_forall_le _ h
+
 /-- A randomized continuation can fail because its precondition was already false or because
 it fails from a valid input. No independence or finite-state assumption is needed. -/
 theorem toOuterMeasure_bind_failure_le (p : PMF α) (kernel : α → PMF β)