refactor(classes): state the Classes area plainly (#456 S2)

Complexity/Computability/Complexity/AffineDisperser.lean

@@ -118,7 +118,7 @@ theorem slice_explicitDisperserLanguage (N : ℕ) :
 /-- **The language of the explicit disperser is in `P`**, with words encoded as themselves. -/
 theorem explicitDisperserLanguage_mem_P :
     (explicitDisperserLanguage : Set (List Bool)) ∈ Complexity.P encBits :=
-  Complexity.ofSlices_mem_P computableTidilyInPolyTime_explicitDisperser
+  Complexity.ofSlices_mem_P computableInPolyTime_explicitDisperser
 
 /-- **An explicit function in `P` with `B₂` circuit complexity `3.5 N - O(N / log N)`**, after
 [MishraSanthanam2026]: some language over `Bool` in `P` (the language of the explicit disperser)

Complexity/Computability/Complexity/Classes/AWPP.lean

@@ -116,14 +116,15 @@ theorem AWPP_subset_PP : AWPP enc ⊆ PP enc := by
 /-- An efficiently computed unary exponent can be padded to a polynomial in input length.
 Multiplying numerator and denominator by the same power of two preserves the ratio. -/
 theorem mem_AWPP_of_polyTime_exponent {g : α → ℤ} {r : α → ℕ}
-    (hg : g ∈ GapP enc) (hr : ComputableTidilyInPolyTime r enc encUnary)
+    (hg : g ∈ GapP enc) (hr : ComputableInPolyTime r enc encUnary)
     (hA : ∀ a, (0 ≤ g a ∧ g a ≤ (2 : ℤ) ^ r a) ∧
       (a ∈ A → 2 * (2 : ℤ) ^ r a ≤ 3 * g a) ∧
       (a ∉ A → 3 * g a ≤ (2 : ℤ) ^ r a)) : A ∈ AWPP enc := by
+  have hr := hr.tidy
   obtain ⟨p, hle⟩ := hr.polyBounded.exists_polynomial
   have hs : ComputableTidilyInPolyTime
       (fun a => 2 ^ (p.eval (enc a).length - r a)) enc encNat := by fun_prop
-  have hsG := SharpP.natCast_mem_GapP (mem_SharpP_of_polyTime hs)
+  have hsG := SharpP.natCast_mem_GapP (mem_SharpP_of_polyTime (.of_tidy hs))
   refine ⟨_, GapP.mul_mem hg hsG, p, fun a => ?_⟩
   have he : (2 : ℤ) ^ p.eval (enc a).length =
       (2 : ℤ) ^ r a * (2 : ℤ) ^ (p.eval (enc a).length - r a) := by
@@ -140,10 +141,11 @@ theorem mem_AWPP_of_polyTime_exponent {g : α → ℤ} {r : α → ℕ}
 /-- Polynomial-time many-one reductions preserve AWPP after dyadic denominator padding. -/
 theorem PolyTimeReducible.mem_AWPP {β : Type} {encB : β ↪ List Bool} {B : Set β}
     (h : PolyTimeReducible enc encB A B) (hB : B ∈ AWPP encB) : A ∈ AWPP enc := by
-  obtain ⟨r, hr, hAB⟩ := polyTimeReducible_iff_tidy.mp h
+  obtain ⟨r, hr, hAB⟩ := h
   obtain ⟨g, hg, p, hB⟩ := hB
   refine mem_AWPP_of_polyTime_exponent (GapP.comp_mem hg hr)
-    (r := fun a => p.eval (encB (r a)).length) (by fun_prop) (fun a => ?_)
+    (r := fun a => p.eval (encB (r a)).length) (.of_tidy (by have hr := hr.tidy; fun_prop))
+    (fun a => ?_)
   simpa only [Function.comp_apply, ← hAB a] using hB (r a)
 
 end Cslib.Complexity

Complexity/Computability/Complexity/Classes/AWPP/Amplification.lean

@@ -117,25 +117,27 @@ private theorem card_majority_eq {β : Type} [Fintype β] (V : β → Bool) (R :
 /-- The majority polynomial is uniformly GapP for polynomial-time unary repetition counts. -/
 theorem majorityPolynomial_mem {α : Type} {enc : α ↪ List Bool} {g D : α → ℤ}
     {r : α → ℕ} (hg : g ∈ GapP enc) (hD : D ∈ GapP enc)
-    (hr : ComputableTidilyInPolyTime r enc encUnary) :
+    (hr : ComputableInPolyTime r enc encUnary) :
     (fun a => majorityPolynomial (g a) (D a) (r a)) ∈ GapP enc := by
   let ones : α × List Bool → ℕ := fun x => x.2.countP id
-  have hones : ComputableTidilyInPolyTime ones (encPair enc encBits) encUnary := by
+  have hones : ComputableInPolyTime ones (encPair enc encBits) encUnary := by
     dsimp [ones]
     fun_prop
-  have hR : ComputableTidilyInPolyTime (fun x : α × List Bool => r x.1)
+  have hR : ComputableInPolyTime (fun x : α × List Bool => r x.1)
       (encPair enc encBits) encUnary := hr.comp (.fst enc encBits)
-  have hz : ComputableTidilyInPolyTime (fun x : α × List Bool => 2 * r x.1 - ones x)
+  have hz : ComputableInPolyTime (fun x : α × List Bool => 2 * r x.1 - ones x)
       (encPair enc encBits) encUnary := by fun_prop
   have hg' := GapP.pow_mem_polyTime (GapP.comp_mem hg (.fst enc encBits)) hones
   have hd' := GapP.pow_mem_polyTime (GapP.comp_mem (GapP.sub_mem' hD hg) (.fst enc encBits)) hz
-  have htest : ComputableTidilyInPolyTime
+  have htest : ComputableInPolyTime
       (fun x : α × List Bool => if r x.1 < ones x then (1 : ℕ) else 0)
-      (encPair enc encBits) encNat := by fun_prop
+      (encPair enc encBits) encNat :=
+    .of_tidy (ComputableTidilyInPolyTime.ite_decide (ComputableTidilyInPolyTime.unary_lt' hR.tidy
+      hones.tidy) (.const 1) (.const 0))
   have hweight := GapP.mul_mem (GapP.mul_mem hg' hd')
     (SharpP.natCast_mem_GapP (mem_SharpP_of_polyTime htest))
   have hsum := GapP.sum_bits_mem hweight
-    (ComputableTidilyInPolyTime.unary_mul.comp ((ComputableTidilyInPolyTime.const 2).prod hr))
+    (ComputableInPolyTime.unary_mul.comp ((ComputableInPolyTime.const 2).prod hr))
   convert hsum using 1
   ext a
   unfold majorityPolynomial
@@ -240,7 +242,7 @@ theorem amplify {α : Type} {enc : α ↪ List Bool} {A : Set α}
       (0 ≤ G a ∧ G a ≤ D) ∧
         (a ∈ A → (2 : ℤ) ^ q.eval (enc a).length * (D - G a) ≤ D) ∧
         (a ∉ A → (2 : ℤ) ^ q.eval (enc a).length * G a ≤ D) := by
-  refine ⟨majorityPolynomial_mem hg (GapP.two_pow_mem p) (by fun_prop), fun a => ?_⟩
+  refine ⟨majorityPolynomial_mem hg (GapP.two_pow_mem p) (.of_tidy (by fun_prop)), fun a => ?_⟩
   obtain ⟨hb, hy, hn⟩ := hA a
   have h := majorityPolynomial_bounds (e := q.eval (enc a).length) hb.1 hb.2
   have he : (12 * q * p).eval (enc a).length =

Complexity/Computability/Complexity/Classes/AWPP/Lowness.lean

@@ -165,7 +165,8 @@ theorem PPWithOracle_eq_PP_of_mem_AWPP (hA : A ∈ AWPP encBits) (enc : α ↪ L
   have hT : ComputableTidilyInPolyTime T enc encUnary := by dsimp [T]; fun_prop
   let e : α → ℕ := fun a => r a + T a + 4
   have he : ComputableTidilyInPolyTime e enc encUnary := by dsimp [e]; fun_prop
-  obtain ⟨H, hH, R, hR, hweights⟩ := exists_AWPP_queryWeights hA hT he
+  obtain ⟨H, hH, R, hR, hweights⟩ := exists_AWPP_queryWeights hA (.of_tidy hT) (.of_tidy he)
+  have hR := hR.tidy
   let input : α × List Bool → List Bool := encPair enc encBits
   let T' : α × List Bool → ℕ := fun x => T x.1
   let R' : α × List Bool → ℕ := fun x => R x.1
@@ -176,16 +177,16 @@ theorem PPWithOracle_eq_PP_of_mem_AWPP (hA : A ∈ AWPP encBits) (enc : α ↪ L
     · dsimp [input]; fun_prop
     · dsimp [T']; fun_prop
     · dsimp [R']; fun_prop
-    · exact GapP.comp_mem hH (by fun_prop)
+    · exact GapP.comp_mem hH (.of_tidy (by fun_prop))
   let S : α → ℤ := fun a => ∑ w : Fin (r a) → Bool, F (a, List.ofFn w)
-  have hS : S ∈ GapP enc := GapP.sum_bits_mem hF hr
+  have hS : S ∈ GapP enc := GapP.sum_bits_mem hF (.of_tidy hr)
   let E : α → ℤ := fun a => 2 ^ (R a * T a)
-  have hE : E ∈ GapP enc := mem_GapP_of_polyTime (by dsimp [E]; fun_prop)
+  have hE : E ∈ GapP enc := mem_GapP_of_polyTime (.of_tidy (by dsimp [E]; fun_prop))
   have hcoef : (fun a => 2 * (2 : ℤ) ^ r a + 1) ∈ GapP enc :=
-    mem_GapP_of_polyTime (by fun_prop)
+    mem_GapP_of_polyTime (.of_tidy (by fun_prop))
   apply mem_PP_iff_exists_GapP.mpr
   refine ⟨fun a => 4 * S a - (2 * (2 : ℤ) ^ r a + 1) * E a,
-    GapP.sub_mem' (GapP.mul_mem (mem_GapP_of_polyTime (by fun_prop)) hS)
+    GapP.sub_mem' (GapP.mul_mem (mem_GapP_of_polyTime (.of_tidy (by fun_prop))) hS)
       (GapP.mul_mem hcoef hE), fun a => ?_⟩
   have herror (w : Fin (r a) → Bool) : (2 : ℤ) ^ (r a + T a + 4) *
       |F (a, List.ofFn w) - E a * (if V (a, List.ofFn w) then 1 else 0)| ≤

Complexity/Computability/Complexity/Classes/AWPP/OracleWeights.lean

@@ -42,20 +42,20 @@ including arbitrary words occurring in a replay state. The requested error expon
 computed in unary and may be zero. -/
 theorem exists_AWPP_queryWeights {α : Type} {enc : α ↪ List Bool} {A : Set (List Bool)}
     (hA : A ∈ AWPP encBits) {T e : α → ℕ}
-    (hT : ComputableTidilyInPolyTime T enc encUnary)
-    (he : ComputableTidilyInPolyTime e enc encUnary) :
+    (hT : ComputableInPolyTime T enc encUnary)
+    (he : ComputableInPolyTime e enc encUnary) :
     ∃ H ∈ GapP (encPair enc encBits), ∃ R : α → ℕ,
-      ComputableTidilyInPolyTime R enc encUnary ∧ ∀ a w,
+      ComputableInPolyTime R enc encUnary ∧ ∀ a w,
         let D := (2 : ℤ) ^ R a
         (0 ≤ H (a, w) ∧ H (a, w) ≤ D) ∧
           (w.take (T a) ∈ A → (2 : ℤ) ^ e a * (D - H (a, w)) ≤ D) ∧
           (w.take (T a) ∉ A → (2 : ℤ) ^ e a * H (a, w) ≤ D) := by
   obtain ⟨g, hg, p, hA⟩ := hA
   let query : α × List Bool → List Bool := fun x => x.2.take (T x.1)
-  have hquery : ComputableTidilyInPolyTime query (encPair enc encBits) encBits := by
+  have hquery : ComputableInPolyTime query (encPair enc encBits) encBits := by
     dsimp [query]
     fun_prop
-  have he' : ComputableTidilyInPolyTime (fun x : α × List Bool => e x.1)
+  have he' : ComputableInPolyTime (fun x : α × List Bool => e x.1)
       (encPair enc encBits) encUnary := he.comp (.fst enc encBits)
   let H₀ : α × List Bool → ℤ := fun x => AWPPAmplification.majorityPolynomial
     (g (query x)) ((2 : ℤ) ^ p.eval (query x).length) (6 * e x.1)
@@ -66,10 +66,10 @@ theorem exists_AWPP_queryWeights {α : Type} {enc : α ↪ List Bool} {A : Set (
     · fun_prop
   let padding : α × List Bool → ℕ := fun x =>
     12 * e x.1 * (p.eval (T x.1) - p.eval (query x).length)
-  have hpadding : ComputableTidilyInPolyTime padding (encPair enc encBits) encUnary := by
+  have hpadding : ComputableInPolyTime padding (encPair enc encBits) encUnary := by
     dsimp [padding]
     fun_prop
-  have hpow : ComputableTidilyInPolyTime (fun x => 2 ^ padding x)
+  have hpow : ComputableInPolyTime (fun x => 2 ^ padding x)
       (encPair enc encBits) encNat := by fun_prop
   let H : α × List Bool → ℤ := fun x => H₀ x * (2 : ℤ) ^ padding x
   have hH : H ∈ GapP (encPair enc encBits) := by

Complexity/Computability/Complexity/Classes/AWPP/WPP.lean

@@ -50,14 +50,14 @@ theorem WPP_subset_AWPP : WPP enc ⊆ AWPP enc := by
   let D a : ℤ := 2 ^ r a
   have hD : D ∈ GapP enc := by
     have := SharpP.natCast_mem_GapP
-      (mem_SharpP_of_polyTime (ComputableTidilyInPolyTime.binary_two_pow.comp hr))
+      (mem_SharpP_of_polyTime (.of_tidy (ComputableTidilyInPolyTime.binary_two_pow.comp hr)))
     simpa only [Function.comp_apply, Nat.cast_pow, Nat.cast_ofNat, D] using this
   let G := g * g
   have hG : G ∈ GapP enc := GapP.mul_mem hg hg
   have hnum := GapP.sub_mem' (GapP.add_mem (GapP.mul_mem hG hD) (GapP.mul_mem hG hD))
     (GapP.mul_mem hG hG)
   refine mem_AWPP_of_polyTime_exponent hnum
-    (ComputableTidilyInPolyTime.unary_add.comp (hr.prod hr)) (fun a => ?_)
+    (.of_tidy (ComputableTidilyInPolyTime.unary_add.comp (hr.prod hr))) (fun a => ?_)
   have hkcast : (k a : ℤ) = f a * f a := Int.toNat_of_nonneg (mul_self_nonneg _)
   have hkpos : 0 < k a := by
     have := mul_self_pos.mpr (hf0 a)

Complexity/Computability/Complexity/Classes/Alternation/Game.lean

@@ -238,10 +238,13 @@ variable {α : Type} {enc : α ↪ List Bool} {A : Set α}
 /-- **Every problem in `AP` has a polynomial-time game verifier.** -/
 theorem exists_isGameVerifier_of_mem_AP (h : A ∈ AP enc) :
     ∃ (p : Polynomial ℕ) (V : α × List Bool → Bool),
-      ComputableTidilyInPolyTime V (encPair enc encBits) encBool ∧ IsGameVerifier enc p V A := by
-  obtain ⟨t, ht, k, State, hfinite, atm, hdecides⟩ := h
-  obtain ⟨c, d, hle⟩ := ht.exists_le
-  exact ⟨_, atm.gameVerifier enc, atm.computableTidilyInPolyTime_gameVerifier,
-    (hdecides.mono hle).isGameVerifier⟩
+      ComputableInPolyTime V (encPair enc encBits) encBool ∧ IsGameVerifier enc p V A := by
+  have this : ∃ (p : Polynomial ℕ) (V : α × List Bool → Bool), ComputableTidilyInPolyTime V
+      (encPair enc encBits) encBool ∧ IsGameVerifier enc p V A := by
+    obtain ⟨t, ht, k, State, hfinite, atm, hdecides⟩ := h
+    obtain ⟨c, d, hle⟩ := ht.exists_le
+    exact ⟨_, atm.gameVerifier enc, atm.computableTidilyInPolyTime_gameVerifier,
+      (hdecides.mono hle).isGameVerifier⟩
+  simpa only [computableInPolyTime_iff_computableTidilyInPolyTime] using this
 
 end Cslib.Complexity

Complexity/Computability/Complexity/Classes/Alternation/GuessVerify.lean

@@ -187,8 +187,10 @@ variable {α : Type} {enc : α ↪ List Bool} {p : Polynomial ℕ} {V : α × Li
 Stockmeyer][ChandraKozenStockmeyer1981]: a problem with a polynomial-time game verifier is decided
 in polynomial time by the guess-then-verify machine, which writes the moves of the two players,
 alternately, and then runs the verifier. -/
-theorem IsGameVerifier.mem_AP (hV : ComputableTidilyInPolyTime V (encPair enc encBits) encBool)
+theorem IsGameVerifier.mem_AP
+    (hV : Turing.MultiTapeTM.ComputableInPolyTime V (encPair enc encBits) encBool)
     (h : IsGameVerifier enc p V A) : A ∈ AP enc := by
+  have hV := hV.tidy
   -- the number of moves, and the word prepared on tape `B`
   set L : α → ℕ := fun a => 2 * p.eval (enc a).length
   have hL : ComputableTidilyInPolyTime L enc encUnary :=

Complexity/Computability/Complexity/Classes/Alternation/NP.lean

@@ -44,7 +44,7 @@ variable {α : Type} {enc : α ↪ List Bool}
 existential, decides the problem within the same polynomial time bound. -/
 theorem NP_subset_AP : NP enc ⊆ AP enc := by
   rintro A ⟨p, V, hV, hA⟩
-  obtain ⟨k, State, hfinite, machine, c, d, hdecides, -⟩ := hA.exists_decidesInTime hV.tidy
+  obtain ⟨k, State, hfinite, machine, c, d, hdecides, -⟩ := hA.exists_decidesInTime hV
   refine ⟨_, .of_forall_le c d fun _ => le_rfl, k, State, hfinite, ⟨machine, fun _ => false⟩,
     fun a => ⟨(hdecides a).1, ?_⟩⟩
   rw [(hdecides a).2]

Complexity/Computability/Complexity/Classes/Alternation/Savitch.lean

@@ -56,7 +56,7 @@ exactly those in `PSPACE` (`Cslib.Complexity.mem_PSPACE_iff_exists_isGameVerifie
 
 * `Cslib.Complexity.alternation_append_iff`: trailing moves that do not matter.
 * `Cslib.Reachability.alternation_midpointGame_iff`: the midpoint game is Savitch's recursion.
-* `Cslib.Complexity.computableTidilyInPolyTime_savitchVerifier`: the game is polynomial-time.
+* `Cslib.Complexity.computableInPolyTime_savitchVerifier`: the game is polynomial-time.
 * `Cslib.Complexity.exists_isGameVerifier_of_mem_PSPACE`: every problem in `PSPACE` has a
   polynomial-time game verifier.
 * `Cslib.Complexity.PSPACE_subset_AP`, `Cslib.Complexity.AP_eq_PSPACE`: `AP = PSPACE`.
@@ -263,8 +263,8 @@ open _root_.Turing _root_.Turing.MultiTapeTM
 
 /-- A level of the midpoint game is polynomial-time. -/
 @[fun_prop]
-theorem computableTidilyInPolyTime_midpointStep :
-    ComputableTidilyInPolyTime (fun p : ℕ × List Bool × List Bool × List Bool =>
+theorem computableInPolyTime_midpointStep :
+    Turing.MultiTapeTM.ComputableInPolyTime (fun p : ℕ × List Bool × List Bool × List Bool =>
       midpointStep p.1 p.2) (encPair encUnary (encPair encBits (encPair encBits encBits)))
       (encPair encBits (encPair encBits encBits)) := by
   unfold midpointStep midpointMoves
@@ -295,9 +295,11 @@ noncomputable def savitchVerifier (x : α × List Bool) : Bool :=
     (MultiTapeNTM.acceptCode (ntm.codeWidth c d (enc x.1))) x.2
 
 /-- The verifier of the midpoint game is polynomial-time. -/
-theorem computableTidilyInPolyTime_savitchVerifier :
-    ComputableTidilyInPolyTime (savitchVerifier (enc := enc) ntm c d) (encPair enc encBits)
+theorem computableInPolyTime_savitchVerifier :
+    Turing.MultiTapeTM.ComputableInPolyTime (savitchVerifier (enc := enc) ntm c d)
+      (encPair enc encBits)
       encBool := by
+  refine .of_tidy ?_
   have hwidth : ComputableTidilyInPolyTime (fun x : α × List Bool => ntm.codeWidth c d (enc x.1))
       (encPair enc encBits) encUnary :=
     (MultiTapeNTM.computableTidilyInPolyTime_codeWidth c d).comp
@@ -317,7 +319,7 @@ theorem computableTidilyInPolyTime_savitchVerifier :
       ((MultiTapeNTM.computableTidilyInPolyTime_acceptCode hwidth).prod
         (ComputableTidilyInPolyTime.snd enc encBits))
   have hloop := ComputableTidilyInPolyTime.iterateWith_of_bounded_growth hw hw hinit
-    computableTidilyInPolyTime_midpointStep
+    computableInPolyTime_midpointStep.tidy
     (growth := fun x => 2 * savitchWidth (enc := enc) ntm c d x.1)
     (ComputableTidilyInPolyTime.polyBounded (by unfold savitchWidth; fun_prop)) fun x s => by
       unfold midpointStep
@@ -345,29 +347,33 @@ space. The game has `2 * ((W + 1) * W)` moves for the width `W` of the codes, pa
 polynomial number. -/
 theorem exists_isGameVerifier_of_mem_PSPACE (h : A ∈ PSPACE enc) :
     ∃ (p : Polynomial ℕ) (V : α × List Bool → Bool),
-      ComputableTidilyInPolyTime V (encPair enc encBits) encBool ∧ IsGameVerifier enc p V A := by
-  obtain ⟨k, State, _, ntm, s, hs, hA⟩ := PSPACE_subset_NPSPACE h
-  obtain ⟨c, d, hcd⟩ := hs.exists_le
-  -- the number of rounds of the game is polynomially bounded
-  have hrounds : ComputableTidilyInPolyTime
-      (fun a => (savitchWidth (enc := enc) ntm c d a + 1) * savitchWidth (enc := enc) ntm c d a)
-      enc encUnary := by
-    have := MultiTapeNTM.computableTidilyInPolyTime_codeWidth (ntm := ntm) (enc := enc) c d
-    unfold savitchWidth
-    fun_prop
-  obtain ⟨p, hr⟩ := hrounds.polyBounded.exists_polynomial
-  refine ⟨p, savitchVerifier (enc := enc) ntm c d,
-    computableTidilyInPolyTime_savitchVerifier ntm c d, fun a => ?_⟩
-  set w := savitchWidth (enc := enc) ntm c d a
-  have hle : 2 * ((w + 1) * w) ≤ 2 * p.eval (enc a).length :=
-    Nat.mul_le_mul_left 2 (hr a)
-  rw [(hA.recognizesInSpace a).2,
-    ← MultiTapeNTM.savitchDecide_eq_true_iff (hA.recognizesInSpace a).1 (hcd a),
-    MultiTapeNTM.savitchDecide,
-    savitch_eq, ← Nat.add_sub_cancel' hle, List.replicate_add, alternation_append_iff
-      fun z => by rw [Cslib.Complexity.sum_replicate_one, savitchVerifier, savitchVerifier,
-        midpointGame_take]]
-  exact (alternation_midpointGame_iff _ _ _).symm
+      Turing.MultiTapeTM.ComputableInPolyTime V (encPair enc encBits) encBool ∧ IsGameVerifier enc p
+        V A := by
+  have this : ∃ (p : Polynomial ℕ) (V : α × List Bool → Bool), ComputableTidilyInPolyTime V
+      (encPair enc encBits) encBool ∧ IsGameVerifier enc p V A := by
+    obtain ⟨k, State, _, ntm, s, hs, hA⟩ := PSPACE_subset_NPSPACE h
+    obtain ⟨c, d, hcd⟩ := hs.exists_le
+    -- the number of rounds of the game is polynomially bounded
+    have hrounds : ComputableTidilyInPolyTime
+        (fun a => (savitchWidth (enc := enc) ntm c d a + 1) * savitchWidth (enc := enc) ntm c d a)
+        enc encUnary := by
+      have := MultiTapeNTM.computableTidilyInPolyTime_codeWidth (ntm := ntm) (enc := enc) c d
+      unfold savitchWidth
+      fun_prop
+    obtain ⟨p, hr⟩ := hrounds.polyBounded.exists_polynomial
+    refine ⟨p, savitchVerifier (enc := enc) ntm c d,
+      (computableInPolyTime_savitchVerifier ntm c d).tidy, fun a => ?_⟩
+    set w := savitchWidth (enc := enc) ntm c d a
+    have hle : 2 * ((w + 1) * w) ≤ 2 * p.eval (enc a).length :=
+      Nat.mul_le_mul_left 2 (hr a)
+    rw [(hA.recognizesInSpace a).2,
+      ← MultiTapeNTM.savitchDecide_eq_true_iff (hA.recognizesInSpace a).1 (hcd a),
+      MultiTapeNTM.savitchDecide,
+      savitch_eq, ← Nat.add_sub_cancel' hle, List.replicate_add, alternation_append_iff
+        fun z => by rw [Cslib.Complexity.sum_replicate_one, savitchVerifier, savitchVerifier,
+          midpointGame_take]]
+    exact (alternation_midpointGame_iff _ _ _).symm
+  simpa only [Turing.MultiTapeTM.computableInPolyTime_iff_computableTidilyInPolyTime] using this
 
 /-- **`PSPACE ⊆ AP`** [Chandra, Kozen and Stockmeyer][ChandraKozenStockmeyer1981]: a problem in
 `PSPACE` is Savitch's midpoint game on the views of a machine deciding it, which the
@@ -384,7 +390,8 @@ theorem AP_eq_PSPACE : AP enc = PSPACE enc :=
 /-- **The problems with polynomial-time game verifiers are exactly those in `PSPACE`.** -/
 theorem mem_PSPACE_iff_exists_isGameVerifier : A ∈ PSPACE enc ↔
     ∃ (p : Polynomial ℕ) (V : α × List Bool → Bool),
-      ComputableTidilyInPolyTime V (encPair enc encBits) encBool ∧ IsGameVerifier enc p V A :=
+      Turing.MultiTapeTM.ComputableInPolyTime V (encPair enc encBits) encBool ∧ IsGameVerifier enc p
+        V A :=
   ⟨exists_isGameVerifier_of_mem_PSPACE, fun ⟨_, _, hV, h⟩ => h.mem_PSPACE hV⟩
 
 end Cslib.Complexity