diff --git a/Complexity/Computability/Complexity/Classes/IP.lean b/Complexity/Computability/Complexity/Classes/IP.lean
index cfbb528610..f1a3e51935 100644
--- a/Complexity/Computability/Complexity/Classes/IP.lean
+++ b/Complexity/Computability/Complexity/Classes/IP.lean
@@ -269,7 +269,7 @@ private theorem isOraclePPTOn_bppVerifier {p : Polynomial ℕ} {V : α × List B
     IsOraclePPTOn enc encBool (bppVerifier enc p V) := by
   have hcount : ComputableTidilyInPolyTime (fun a => p.eval (enc a).length) enc encUnary := by
     fun_prop
-  exact (IsPPTOn.map_with (f := fun a r => V (a, r)) hcount.sampleList hV).isOraclePPTOn
+  exact (IsPPTOn.map_with (f := fun a r => V (a, r)) hcount.sampleList (.of_tidy hV)).isOraclePPTOn
 
 /-- The verifier without messages accepts every prover with the fraction of accepted random
 strings. -/
diff --git a/Complexity/Computability/Complexity/Classes/IP/GraphNonIsomorphism.lean b/Complexity/Computability/Complexity/Classes/IP/GraphNonIsomorphism.lean
index 6aeb7a9655..a6dc9d3419 100644
--- a/Complexity/Computability/Complexity/Classes/IP/GraphNonIsomorphism.lean
+++ b/Complexity/Computability/Complexity/Classes/IP/GraphNonIsomorphism.lean
@@ -570,7 +570,7 @@ private theorem isPPTOn_relabelMessage {γ : Type} {input : γ ↪ List Bool} {G
         (fst (encPair input encBits) encBits))) (snd (encPair input encBits) encBits))
   exact IsPPTOn.map_with (f := fun x bits => relabel (G x) (keysOf (G x).distinctVertices.length
     (keyWidth (G x).distinctVertices.length) bits)) hcount.sampleList
-    (computableTidilyInPolyTime_relabel (hG.comp (fst input encBits)) hkeys)
+    (.of_tidy (computableTidilyInPolyTime_relabel (hG.comp (fst input encBits)) hkeys))
 
 /-- The verifier is strict oracle PPT. -/
 theorem isOraclePPTOn_verifier :
diff --git a/Complexity/Computability/Complexity/Classes/NP/GuessVerify.lean b/Complexity/Computability/Complexity/Classes/NP/GuessVerify.lean
index a38dacb5d1..fce7c79b21 100644
--- a/Complexity/Computability/Complexity/Classes/NP/GuessVerify.lean
+++ b/Complexity/Computability/Complexity/Classes/NP/GuessVerify.lean
@@ -68,7 +68,7 @@ theorem IsVerifier.exists_decidesInTime
     (fun w => V (a, w)) <$> BitString.sampleList (p.eval (enc a).length)
   have hcount : ComputableTidilyInPolyTime (fun a => p.eval (enc a).length) enc encUnary :=
     (ComputableTidilyInPolyTime.unary_eval p).comp (ComputableTidilyInPolyTime.encoding_length enc)
-  have hprogram : IsPPTOn enc encBool program := hcount.sampleList.map_with hV
+  have hprogram : IsPPTOn enc encBool program := hcount.sampleList.map_with (.of_tidy hV)
   obtain ⟨k, State, hfinite, machine, c, d, heval, hhalt⟩ := hprogram.exists_halting_machine
   refine ⟨k, State, hfinite, machine, c, d, fun a => ?_, fun _ => machine.exists_step_toNTM⟩
   have htime : machine.toNTM.RunsInTime (enc a) (c * ((enc a).length + 1) ^ d) :=
diff --git a/Complexity/Computability/Complexity/Classes/Padding.lean b/Complexity/Computability/Complexity/Classes/Padding.lean
index 6b7c9ad62d..d87f526b6f 100644
--- a/Complexity/Computability/Complexity/Classes/Padding.lean
+++ b/Complexity/Computability/Complexity/Classes/Padding.lean
@@ -335,7 +335,7 @@ theorem preimage_mem_NTIME_of_mem_NP {B : Set (List Bool)} {g : α → List Bool
   have hcount : ComputableTidilyInPolyTime (fun x : List Bool => p.eval x.length)
       encBits encUnary :=
     (unary_eval p).comp (encoding_length encBits)
-  have hprogram : IsPPTOn encBits encBool program := hcount.sampleList.map_with hV.tidy
+  have hprogram : IsPPTOn encBits encBool program := hcount.sampleList.map_with hV
   obtain ⟨k₁, State₁, hfinite₁, M_NP, c₁, d₁, heval₂, hhalt₂⟩ := hprogram.exists_halting_machine
   set t₂ : α → ℕ := fun a => c₁ * (t₁ a + 1) ^ d₁
   have ht₂_le (a : α) : c₁ * ((g a).length + 1) ^ d₁ ≤ t₂ a :=
diff --git a/Complexity/Computability/Complexity/Classes/Promise/Reduction.lean b/Complexity/Computability/Complexity/Classes/Promise/Reduction.lean
index 061cb9a3c9..5c30473093 100644
--- a/Complexity/Computability/Complexity/Classes/Promise/Reduction.lean
+++ b/Complexity/Computability/Complexity/Classes/Promise/Reduction.lean
@@ -373,7 +373,7 @@ private theorem isPPTOn_sampleList_verifier {p : Polynomial ℕ} {V : α × List
   have hcount : ComputableTidilyInPolyTime (fun a => p.eval (enc a).length) enc encUnary :=
     (ComputableTidilyInPolyTime.unary_eval p).comp
       (ComputableTidilyInPolyTime.encoding_length enc)
-  hcount.sampleList.map_with hV
+  hcount.sampleList.map_with (.of_tidy hV)
 
 /-- **Probabilistic-program characterization of `PromiseBPP`**: a promise problem is in
 `PromiseBPP` exactly when a uniform strict PPT Boolean program accepts every yes-instance with
@@ -804,7 +804,7 @@ theorem rpReducible_iff_exists_seeded :
         (ComputableTidilyInPolyTime.encoding_length encA)
     let R (a : α) : ProbComp β :=
       (fun w => f (a, w)) <$> BitString.sampleList (p.eval (encA a).length)
-    have hR : IsPPTOn encA encB R := hcount.sampleList.map_with hf.tidy
+    have hR : IsPPTOn encA encB R := hcount.sampleList.map_with hf
     refine ⟨R, hR, fun a ha b hb => ?_, fun a ha => ?_⟩
     · simp only [R, ProbComp.eval_map, BitString.eval_sampleList,
         PMF.mem_support_map_iff, BitString.mem_support_uniformList_iff] at hb
diff --git a/Complexity/Computability/Complexity/Classes/Time.lean b/Complexity/Computability/Complexity/Classes/Time.lean
index 1dbee02714..1788883e9a 100644
--- a/Complexity/Computability/Complexity/Classes/Time.lean
+++ b/Complexity/Computability/Complexity/Classes/Time.lean
@@ -426,7 +426,7 @@ theorem mem_BPP_iff_exists_mem_BPTIME {α : Type} {enc : α ↪ List Bool} {A :
     have hcount : ComputableTidilyInPolyTime (fun a => p.eval (enc a).length) enc encUnary :=
       (ComputableTidilyInPolyTime.unary_eval p).comp
         (ComputableTidilyInPolyTime.encoding_length enc)
-    have hprogram : IsPPTOn enc encBool program := hcount.sampleList.map_with hV
+    have hprogram : IsPPTOn enc encBool program := hcount.sampleList.map_with (.of_tidy hV)
     obtain ⟨k, State, hfinite, machine, c, d, heval, hhalt⟩ := hprogram.exists_halting_machine
     refine ⟨d, c * 2 ^ d, c, k, State, hfinite, machine,
       MultiTapePTM.DecidesWithBoundedErrorInTime.mono (t := fun a => c * ((enc a).length + 1) ^ d)
diff --git a/Complexity/Computability/Probabilistic/BoundedUniform.lean b/Complexity/Computability/Probabilistic/BoundedUniform.lean
index b76b317e01..e6f1f2e926 100644
--- a/Complexity/Computability/Probabilistic/BoundedUniform.lean
+++ b/Complexity/Computability/Probabilistic/BoundedUniform.lean
@@ -53,7 +53,7 @@ theorem isPPTOn_sampleUniformInterval {α : Type} {input : α ↪ List Bool}
   have hfind : ComputableTidilyInPolyTime
       (fun p : α × List ℕ => p.2.find? (fun value => decide (value < bound p.1)))
       (encPair input (encList encUnary)) (encOption encUnary) := by fun_prop
-  exact hs.map_with hfind
+  exact hs.map_with (.of_tidy hfind)
 
 /-- Binary bounds need only a unary sampling width and attempt count. The width is the existing
 sampler's computed `log₂ bound + 1`, not a unary copy of `bound`; exponential cryptographic
@@ -80,7 +80,7 @@ theorem isPPTOn_sampleUniformInterval_binary {α : Type} {input : α ↪ List Bo
     simp only [min_def, Function.comp_def, decide_eq_true_eq]
   have hs : IsPPTOn input encNat (fun a => sampleBoundedIndex (bound a)) := by
     apply ((isPPTOn_sampleBinaryNat.preprocess hw).map_with
-      (f := fun a value => min (bound a) value) hmin).congr
+      (f := fun a value => min (bound a) value) (.of_tidy hmin)).congr
     intro a
     rw [sampleBoundedIndex_eq_binary, ← hwidth_eq a]
   have hfind : ComputableTidilyInPolyTime
@@ -89,7 +89,7 @@ theorem isPPTOn_sampleUniformInterval_binary {α : Type} {input : α ↪ List Bo
     apply ComputableTidilyInPolyTime.findWithInput (by fun_prop)
     exact ComputableTidilyInPolyTime.binary_lt.comp
       ((ComputableTidilyInPolyTime.snd _ _).prod (by fun_prop))
-  exact (hs.replicate ha).map_with hfind
+  exact (hs.replicate ha).map_with (.of_tidy hfind)
 
 /-- A runtime-varying integer box is sampled in uniform strict PPT when the numerical radius,
 dimension and per-coordinate attempt budget are efficiently supplied in unary. The full
@@ -122,7 +122,7 @@ theorem isPPTOn_sampleIntegerBox {α : Type} {input : α ↪ List Bool}
       (encList (encOption encInt)) (encOption (encList encInt)) := by
     unfold collectBox
     fun_prop
-  exact (((hs.map_with hcoordinate).replicate hd).map hcollect)
+  exact (((hs.map_with (.of_tidy hcoordinate)).replicate hd).map hcollect)
 
 /-- The complete framed optional output has a direct linear bound in dimension and unary
 radius; failure encodes as the empty word. -/
diff --git a/Complexity/Computability/Probabilistic/CenteredBinomial.lean b/Complexity/Computability/Probabilistic/CenteredBinomial.lean
index 77f156a605..48dcd62485 100644
--- a/Complexity/Computability/Probabilistic/CenteredBinomial.lean
+++ b/Complexity/Computability/Probabilistic/CenteredBinomial.lean
@@ -56,7 +56,7 @@ theorem isPPTOn_sampleCenteredBinomial :
         (hcast.comp (ComputableTidilyInPolyTime.snd _ _)))
   have hsecond := (hcount.preprocess
     (ComputableTidilyInPolyTime.fst encUnary encUnary)).map_with
-      (f := fun (p : ℕ × ℕ) (negative : ℕ) => (p.2 : ℤ) - negative) hsub
+      (f := fun (p : ℕ × ℕ) (negative : ℕ) => (p.2 : ℤ) - negative) (.of_tidy hsub)
   unfold sampleCenteredBinomial
   apply hcount.bind_with
   simpa only [bind_pure_comp] using hsecond
diff --git a/Complexity/Computability/Probabilistic/Memoize.lean b/Complexity/Computability/Probabilistic/Memoize.lean
index 8eb76380c5..d03b6b6d80 100644
--- a/Complexity/Computability/Probabilistic/Memoize.lean
+++ b/Complexity/Computability/Probabilistic/Memoize.lean
@@ -76,7 +76,7 @@ theorem IsPPTOn.memoize {α Key Value : Type} [BEq Key] [LawfulBEq Key] {input :
       (encPair valueEncoding (encList (encPair keyEncoding valueEncoding))) := by
     unfold finish
     fun_prop
-  refine (hcompute.map_with (f := finish) hpost).congr ?_
+  refine (hcompute.map_with (f := finish) (.of_tidy hpost)).congr ?_
   intro a
   rw [Cslib.memoize, lookup_eq_map_find]
   cases h : (cache a).find? (fun entry => query a == entry.1) <;>
diff --git a/Complexity/Computability/Probabilistic/PPT/Capture.lean b/Complexity/Computability/Probabilistic/PPT/Capture.lean
index 12b53dc3d7..4efb15acd3 100644
--- a/Complexity/Computability/Probabilistic/PPT/Capture.lean
+++ b/Complexity/Computability/Probabilistic/PPT/Capture.lean
@@ -8,6 +8,7 @@ module
 -- upstream: candidate
 
 public import Complexity.Computability.Probabilistic.PPT.Composition
+public import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Plain
 public import Complexity.Computability.Machines.Turing.MultiTape.Probabilistic.OutputPrefix
 import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.List
 import Complexity.Computability.Probabilistic.Oracle.Composition
@@ -85,10 +86,10 @@ theorem IsPPTOn.bind_with {first : α → ProbComp β} {second : α → β → P
 @[fun_prop]
 theorem IsPPTOn.map_with {program : α → ProbComp β} {f : α → β → γ}
     (hprogram : IsPPTOn input left program)
-    (hf : ComputableTidilyInPolyTime (fun pair => f pair.1 pair.2) (encPair input left) right) :
+    (hf : ComputableInPolyTime (fun pair => f pair.1 pair.2) (encPair input left) right) :
     IsPPTOn input right (fun a => f a <$> program a) := by
   simpa only [bind_pure_comp] using
-    hprogram.bind_with (right := right) (second := fun a b => pure (f a b)) hf.isPPTOn
+    hprogram.bind_with (right := right) (second := fun a b => pure (f a b)) hf.tidy.isPPTOn
 
 /-- Select a closed probabilistic branch with an efficient Boolean condition, using the
 empty-channel specialization of oracle branch selection. -/
diff --git a/Complexity/Computability/Probabilistic/Repeat.lean b/Complexity/Computability/Probabilistic/Repeat.lean
index 88e7e0b44a..79b56dc149 100644
--- a/Complexity/Computability/Probabilistic/Repeat.lean
+++ b/Complexity/Computability/Probabilistic/Repeat.lean
@@ -63,7 +63,7 @@ theorem IsPPTOn.replicate {α β : Type} {input : α ↪ List Bool} {output : β
     (ComputableTidilyInPolyTime.fst input encBits) hrows
   have hcoins := (ComputableTidilyInPolyTime.unary_mul.comp (hcount.prod hbudget)).sampleList
   apply (hcoins.map_with (f := fun a coins =>
-    (BitString.listRows (count a) (budget a) coins).map (evaluate a)) hmap).congr
+    (BitString.listRows (count a) (budget a) coins).map (evaluate a)) (.of_tidy hmap)).congr
   intro a
   simpa only [ProbComp.eval_map, BitString.eval_sampleList, Function.comp_def] using
     (ProbComp.eval_replicate_of_uniformList (count a) (budget a)
diff --git a/Complexity/Computability/Probabilistic/Selection.lean b/Complexity/Computability/Probabilistic/Selection.lean
index 082b0599ca..d68c3b6ebc 100644
--- a/Complexity/Computability/Probabilistic/Selection.lean
+++ b/Complexity/Computability/Probabilistic/Selection.lean
@@ -58,6 +58,7 @@ theorem IsPPTOn.selectBest {α : Type} {input : α ↪ List Bool}
       (fun pair => OracleComp.selectStep (trials pair.1) (test pair.1) pair.2) := by
     unfold OracleComp.selectStep
     apply (htest'.countTrue htrials').map_with
+    apply ComputableInPolyTime.of_tidy
     dsimp only [OracleComp.selectUpdate, stateEncoding]
     polytime
   have hloop := (IsPPTOn.iterateWith_spec (stateEncoding := stateEncoding)
@@ -83,6 +84,11 @@ theorem IsPPTOn.selectFrom {α β : Type} {input : α ↪ List Bool} {output : 
     (htest : IsPPTOn (encPair input output) encBool (fun pair => test pair.1 pair.2)) :
     IsPPTOn input output
       (fun a => OracleComp.selectFrom (values a) (trials a) (test a) fallback) := by
+  have hget : ComputableInPolyTime
+      (fun p : α × ℕ => ((values p.1)[p.2]?).getD fallback)
+      (encPair input encUnary) output := by
+    apply ComputableInPolyTime.of_tidy
+    fun_prop
   unfold OracleComp.selectFrom
   ppt
 
diff --git a/Complexity/Computability/Probabilistic/Traverse.lean b/Complexity/Computability/Probabilistic/Traverse.lean
index 1795d1c4aa..846afc4e74 100644
--- a/Complexity/Computability/Probabilistic/Traverse.lean
+++ b/Complexity/Computability/Probabilistic/Traverse.lean
@@ -93,7 +93,7 @@ theorem IsPPTOn.mapM {α β : Type} {input : α ↪ List Bool} {output : β ↪
         (encPair input encBits) by fun_prop)
   have hcoins := (ComputableTidilyInPolyTime.unary_mul.comp (hcount.prod hbudget)).sampleList
   apply (hcoins.map_with (f := fun list tape => list.zipIdx.map
-    (fun q => evaluate q.1 (BitString.listRow (budget list) q.2 tape))) hrun).congr
+    (fun q => evaluate q.1 (BitString.listRow (budget list) q.2 tape))) (.of_tidy hrun)).congr
   intro list
   rw [ProbComp.eval_map, BitString.eval_sampleList]
   symm
diff --git a/Complexity/Computability/Probabilistic/UniformNat.lean b/Complexity/Computability/Probabilistic/UniformNat.lean
index 7a4869c3ed..b5ad0445a3 100644
--- a/Complexity/Computability/Probabilistic/UniformNat.lean
+++ b/Complexity/Computability/Probabilistic/UniformNat.lean
@@ -87,8 +87,12 @@ theorem isPPTOn_sampleDyadicCoin {α : Type} {input : α ↪ List Bool}
     (hbound : ComputableTidilyInPolyTime bound input encUnary)
     (hnumerator : ComputableTidilyInPolyTime numerator input encUnary) :
     IsPPTOn input encBool (fun a => sampleDyadicCoin (bound a) (numerator a)) := by
-  unfold sampleDyadicCoin
-  ppt
+  have hcallback : ComputableInPolyTime
+      (fun p : α × ℕ => decide (p.2 < numerator p.1)) (encPair input encUnary) encBool := by
+    apply ComputableInPolyTime.of_tidy
+    fun_prop
+  simpa only [sampleDyadicCoin, bind_pure_comp] using
+    (isPPTOn_sampleDyadicIndex hbound).map_with hcallback
 
 /-- An efficiently supplied unary bound gives a strict PPT capped index sampler. -/
 @[program_certificate]
@@ -121,6 +125,7 @@ theorem isPPTOn_sampleModNat {α : Type} {input : α ↪ List Bool} {width modul
     IsPPTOn input encNat (fun a => sampleModNat (width a) (modulus a)) := by
   unfold sampleModNat
   exact (ComputableTidilyInPolyTime.sampleBinaryNat hwidth.tidy).map_with
-    (ComputableTidilyInPolyTime.binary_mod' (by fun_prop) (hmodulus.tidy.comp (by fun_prop)))
+    (.of_tidy (ComputableTidilyInPolyTime.binary_mod' (by fun_prop)
+      (hmodulus.tidy.comp (by fun_prop))))
 
 end Cslib.Probability
diff --git a/Complexity/Crypto/Computational/GoldreichLevin/WordReduction.lean b/Complexity/Crypto/Computational/GoldreichLevin/WordReduction.lean
index 6908985fd5..ed2ab980e6 100644
--- a/Complexity/Crypto/Computational/GoldreichLevin/WordReduction.lean
+++ b/Complexity/Crypto/Computational/GoldreichLevin/WordReduction.lean
@@ -97,6 +97,15 @@ theorem isPPT_wordInverter {f : List Bool → List Bool}
       (fun p : (ℕ × List Bool) × List Bool => evaluate p.1 p.2)
       (encPair (encPair encUnary encBits) encBits) encBool)
     (c d degree : ℕ) : IsPPT encBits (wordInverter f evaluate c d degree) := by
+  have hdecode : ComputableInPolyTime
+      (fun p : (((ℕ × List Bool) × Bool) × List Bool) × List Bool =>
+        wordDecode f
+          (fun query => evaluate (p.1.1.1.1, p.1.1.1.2 ++ query) p.1.2 ^^ p.1.1.2)
+          degree p.1.1.1.1 p.1.1.1.2 p.2)
+      (encPair (encPair (encPair (encPair encUnary encBits) encBool) encBits) encBits)
+      encBits := by
+    apply ComputableInPolyTime.of_tidy
+    fun_prop
   unfold wordInverter coinBudget
   ppt
 
diff --git a/Complexity/Crypto/Computational/Homomorphic/Evaluation/PolyTime.lean b/Complexity/Crypto/Computational/Homomorphic/Evaluation/PolyTime.lean
index c53ab65df1..30bb356af3 100644
--- a/Complexity/Crypto/Computational/Homomorphic/Evaluation/PolyTime.lean
+++ b/Complexity/Crypto/Computational/Homomorphic/Evaluation/PolyTime.lean
@@ -64,6 +64,7 @@ theorem isPPTOn_evaluateCircuit (D : DecryptionCircuits E secretWidth ciphertext
     hcode)).tidy
   apply (isPPTOn_evaluateLayers D hencrypt hevaluate hD hn hpks heks hinputs
     hcompiled.fst').map_with
+  apply Turing.MultiTapeTM.ComputableInPolyTime.of_tidy
   apply ComputableTidilyInPolyTime.mapWithInput
     (hcompiled.snd'.comp (ComputableTidilyInPolyTime.fst _ _))
   exact ComputableTidilyInPolyTime.listGetD_binary [] (by fun_prop) (by fun_prop)
diff --git a/Complexity/Crypto/Computational/Homomorphic/FixedKey/PolyTime.lean b/Complexity/Crypto/Computational/Homomorphic/FixedKey/PolyTime.lean
index 7da3af7ad0..a2ecd5c5ca 100644
--- a/Complexity/Crypto/Computational/Homomorphic/FixedKey/PolyTime.lean
+++ b/Complexity/Crypto/Computational/Homomorphic/FixedKey/PolyTime.lean
@@ -68,14 +68,14 @@ theorem isPPTOn_keyGen
     (ComputableTidilyInPolyTime.snd _ _).fst'
     (ComputableTidilyInPolyTime.snd _ _).snd'
   simpa only [bind_pure_comp] using hbits.map_with
-    (show ComputableTidilyInPolyTime
+    (.of_tidy (show ComputableTidilyInPolyTime
       (fun p : (α × (List Bool × List Bool)) × List (List Bool) =>
         (encPublicKey (p.1.2.1, p.2), p.1.2.2))
       (encPair (encPair input (encPair encBits encBits)) (encList encBits))
       (encPair encBits encBits) from
       (((ComputableTidilyInPolyTime.fst _ _).snd'.fst'.prod
         (ComputableTidilyInPolyTime.snd _ _)).encoded).prod
-          (ComputableTidilyInPolyTime.fst _ _).snd'.snd')
+          (ComputableTidilyInPolyTime.fst _ _).snd'.snd'))
 
 include hencrypt in
 /-- Decode any public word and encrypt under the decoded base public key. -/
diff --git a/Complexity/Crypto/Computational/Homomorphic/Layered/PolyTime.lean b/Complexity/Crypto/Computational/Homomorphic/Layered/PolyTime.lean
index 7331fa916c..665daa374a 100644
--- a/Complexity/Crypto/Computational/Homomorphic/Layered/PolyTime.lean
+++ b/Complexity/Crypto/Computational/Homomorphic/Layered/PolyTime.lean
@@ -99,9 +99,9 @@ theorem isPPTOn_evaluateNode
   have hcap := (computableTidilyInPolyTime_decryptionArity D hD).comp hn
   have hbounded := hraw.map_with (f := fun a ciphertext =>
     ciphertext.take (secretWidth (n a) + ciphertextWidth (n a)))
-    (ComputableTidilyInPolyTime.bitsTake.comp
+    (.of_tidy (ComputableTidilyInPolyTime.bitsTake.comp
       ((ComputableTidilyInPolyTime.snd input encBits).prod
-        (hcap.comp (ComputableTidilyInPolyTime.fst input encBits))))
+        (hcap.comp (ComputableTidilyInPolyTime.fst input encBits)))))
   apply hbounded.congr
   intro a
   cases node a <;> rfl
diff --git a/Complexity/Crypto/Computational/Homomorphic/Leveled/PolyTime.lean b/Complexity/Crypto/Computational/Homomorphic/Leveled/PolyTime.lean
index 1df2eff7df..380491a976 100644
--- a/Complexity/Crypto/Computational/Homomorphic/Leveled/PolyTime.lean
+++ b/Complexity/Crypto/Computational/Homomorphic/Leveled/PolyTime.lean
@@ -83,6 +83,7 @@ theorem isPPTOn_keyGen
     IsPPTOn input (encPair encBits encBits) (fun a => keyGen E (n a) (budget a)) := by
   apply (Scheme.isPPTOn_generateKeyChain hkeyGen hencrypt hn
     (show ComputableTidilyInPolyTime (fun a => 2 * budget a) input encUnary by fun_prop)).map_with
+  apply Turing.MultiTapeTM.ComputableInPolyTime.of_tidy
   apply computableTidilyInPolyTime_keyPair <;> fun_prop
 
 include hencrypt in
@@ -146,6 +147,7 @@ theorem isPPTOn_evaluateCircuit {inputCount : α → ℕ}
     (.of_tidy hcompiled.fst')).tidy
   apply (Scheme.isPPTOn_evaluateLayers D hencrypt hevaluate hD hn hpks hlinks hinputs
     hpadded).map_with
+  apply Turing.MultiTapeTM.ComputableInPolyTime.of_tidy
   apply ComputableTidilyInPolyTime.mapWithInput
     (hcompiled.snd'.comp (ComputableTidilyInPolyTime.fst _ _))
   exact ComputableTidilyInPolyTime.listGetD_binary [] (by fun_prop) (by fun_prop)
diff --git a/Complexity/Crypto/Computational/OneWay/BPP.lean b/Complexity/Crypto/Computational/OneWay/BPP.lean
index 533e325de6..fee068c99d 100644
--- a/Complexity/Crypto/Computational/OneWay/BPP.lean
+++ b/Complexity/Crypto/Computational/OneWay/BPP.lean
@@ -99,7 +99,7 @@ theorem isPPT_randomizedPreimageSearch {p : Polynomial ℕ}
     exact (unary_eval p).comp ((encoding_length encPreimagePrefix).comp
       ((fst _ _).prod ((snd _ _).prod ((bitsReplicate false).comp (fst _ _)))))
   refine IsPPTOn.map_with hlen.sampleList
-    (computableTidilyInPolyTime_preimageSearch_of_input ?_ (fst _ _))
+    (.of_tidy (computableTidilyInPolyTime_preimageSearch_of_input ?_ (fst _ _)))
   exact hV.comp ((snd _ _).prod (bitsTakeWithInput (fst _ _).snd'
     ((unary_eval p).comp ((encoding_length encPreimagePrefix).comp (snd _ _)))))
 
diff --git a/Complexity/Crypto/Computational/OneWay/MCSP.lean b/Complexity/Crypto/Computational/OneWay/MCSP.lean
index 417ed5b457..4b484a5c47 100644
--- a/Complexity/Crypto/Computational/OneWay/MCSP.lean
+++ b/Complexity/Crypto/Computational/OneWay/MCSP.lean
@@ -142,7 +142,7 @@ theorem isPPTOn_mcspRun
     (hV : ComputableTidilyInPolyTime V (encPair MCSP.encInstance encBits) encBool) :
     IsPPTOn MCSP.encInstance encBool (mcspRun p V) :=
   IsPPTOn.map_with (ComputableTidilyInPolyTime.sampleList
-    ((unary_eval p).comp (encoding_length MCSP.encInstance))) hV
+    ((unary_eval p).comp (encoding_length MCSP.encInstance))) (.of_tidy hV)
 
 /-- The acceptance probability of `mcspRun` is the fraction of accepting coin strings. -/
 theorem toReal_eval_mcspRun (p : Polynomial ℕ) (V : MCSP.Instance × List Bool → Bool)
diff --git a/ComplexityTests.lean b/ComplexityTests.lean
index 1f459e0589..0e9b487a43 100644
--- a/ComplexityTests.lean
+++ b/ComplexityTests.lean
@@ -342,6 +342,7 @@ import ComplexityTests.PPTruthTable
 import ComplexityTests.PRGStretch
 import ComplexityTests.Parameterized
 import ComplexityTests.PlainAutomationSupport
+import ComplexityTests.PlainCapturedMap
 import ComplexityTests.PlainLawfulBEq
 import ComplexityTests.PolySpaceFold
 import ComplexityTests.PolyTimeBinaryWord
diff --git a/ComplexityTests/PlainCapturedMap.lean b/ComplexityTests/PlainCapturedMap.lean
new file mode 100644
index 0000000000..f9dbababcf
--- /dev/null
+++ b/ComplexityTests/PlainCapturedMap.lean
@@ -0,0 +1,41 @@
+/-
+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.Computability.Probabilistic.PPT.Capture
+import Complexity.Tactic.PPT
+
+/-!
+# Plain deterministic callbacks with captured probabilistic input
+
+The callback is certified on the entire framed pair of caller input and sampled value. It uses
+one uniform machine, with no separate premise about the sampled value's length or distribution.
+-/
+
+open Cslib Cslib.Probability Turing.MultiTapeTM
+
+example {α β γ : Type} {input : α ↪ List Bool} {sample : β ↪ List Bool}
+    {output : γ ↪ List Bool} {program : α → ProbComp β} {callback : α → β → γ}
+    (hp : IsPPTOn input sample program)
+    (hf : ComputableInPolyTime (fun p => callback p.1 p.2) (encPair input sample) output) :
+    IsPPTOn input output (fun a => callback a <$> program a) := by
+  fail_if_success (clear hf; ppt)
+  exact hp.map_with hf
+
+-- A raw construction certificate can still be explicitly forgotten inside an existing proof.
+example {α β γ : Type} {input : α ↪ List Bool} {sample : β ↪ List Bool}
+    {output : γ ↪ List Bool} {program : α → ProbComp β} {callback : α → β → γ}
+    (hp : IsPPTOn input sample program)
+    (hf : ComputableTidilyInPolyTime (fun p => callback p.1 p.2) (encPair input sample) output) :
+    IsPPTOn input output (fun a => callback a <$> program a) :=
+  hp.map_with (.of_tidy hf)
+
+-- The output retains an actual captured word as well as the sampled word.
+example {source : ℕ × List Bool → ProbComp (List Bool)}
+    (hs : IsPPTOn (encPair encUnary encBits) encBits source) :
+    IsPPTOn (encPair encUnary encBits) encBits
+      (fun a => (fun word => a.2 ++ word) <$> source a) := by
+  apply hs.map_with
+  fun_prop
diff --git a/scripts/tidy_surface_baseline.json b/scripts/tidy_surface_baseline.json
index 73aa341ac5..1ad1cfe155 100644
--- a/scripts/tidy_surface_baseline.json
+++ b/scripts/tidy_surface_baseline.json
@@ -296,7 +296,7 @@
  "Complexity/Computability/Probabilistic/Oracle/Tidy.lean": 18,
  "Complexity/Computability/Probabilistic/OracleSimulation.lean": 1,
  "Complexity/Computability/Probabilistic/PPT.lean": 1,
- "Complexity/Computability/Probabilistic/PPT/Capture.lean": 5,
+ "Complexity/Computability/Probabilistic/PPT/Capture.lean": 4,
  "Complexity/Computability/Probabilistic/PPT/Composition.lean": 2,
  "Complexity/Computability/Probabilistic/Parameter.lean": 2,
  "Complexity/Computability/Probabilistic/Presample.lean": 2,