diff --git a/Complexity/Computability/Machines/Turing/MultiTape/Complexity/PolySpace/Plain.lean b/Complexity/Computability/Machines/Turing/MultiTape/Complexity/PolySpace/Plain.lean
index 9a5aa35d6c..8caffdcea8 100644
--- a/Complexity/Computability/Machines/Turing/MultiTape/Complexity/PolySpace/Plain.lean
+++ b/Complexity/Computability/Machines/Turing/MultiTape/Complexity/PolySpace/Plain.lean
@@ -9,7 +9,9 @@ module
 
 public import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolySpace
 public import Complexity.Computability.Machines.Turing.MultiTape.ResourceBounds
+public import Complexity.Computability.Machines.Turing.MultiTape.PolyTime
 import Complexity.Computability.Machines.Turing.MultiTape.Complexity.BigO.Plain
+import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Plain
 
 /-!
 # Polynomial space on plain machines
@@ -21,18 +23,28 @@ form changes the bounds by constant factors
 notions with `Turing.MultiTapeTM.ComputableInPolySpace.tidy` and
 `Turing.MultiTapeTM.ComputableInPolySpace.of_tidy`.
 
+The plain predicate and its closure rules are registered with `fun_prop`. A plain goal can use
+plain polynomial-space and polynomial-time hypotheses, together with tidy certificates through
+`Turing.MultiTapeTM.ComputableTidilyInPolySpace.computableInPolySpace`. Only the tidy-to-plain
+direction is a transition rule; the reverse bridge is used explicitly inside the proofs.
+
 ## Main results
 
 * `Turing.MultiTapeTM.computableInPolySpace_iff_computableTidilyInPolySpace`: the plain and tidy
   notions agree, with the shortcuts `Turing.MultiTapeTM.ComputableInPolySpace.tidy`,
   `Turing.MultiTapeTM.ComputableInPolySpace.of_tidy` and
   `Turing.MultiTapeTM.ComputableTidilyInPolySpace.computableInPolySpace`.
+* `Turing.MultiTapeTM.ComputableInPolySpace.of_polyTime`: plain polynomial time is within
+  polynomial space.
+* `Turing.MultiTapeTM.ComputableInPolySpace.comp`, `.prod`, `.ite`: closure properties.
 -/
 
 @[expose] public section
 
 namespace Turing.MultiTapeTM
 
+attribute [fun_prop] ComputableInPolySpace
+
 variable {α β : Type} {f : α → β} {encIn : α ↪ List Bool} {encOut : β ↪ List Bool}
 
 /-- A function computable within polynomial space is tidily computable within polynomial space. -/
@@ -51,7 +63,9 @@ theorem ComputableInPolySpace.of_tidy (h : ComputableTidilyInPolySpace f encIn e
   exact ⟨_, fun n => c * (b n + 1), by fun_prop,
     hc.computableInTimeAndSpace.mono (fun _ => le_rfl) hcS, fun a => (hl a).trans (hcS a)⟩
 
-/-- `Turing.MultiTapeTM.ComputableInPolySpace.of_tidy` for dot notation on a tidy hypothesis. -/
+/-- `Turing.MultiTapeTM.ComputableInPolySpace.of_tidy` for dot notation on a tidy hypothesis and
+the transition used by `fun_prop` to prove plain goals from tidy certificates. -/
+@[fun_prop]
 theorem ComputableTidilyInPolySpace.computableInPolySpace
     (h : ComputableTidilyInPolySpace f encIn encOut) : ComputableInPolySpace f encIn encOut :=
   .of_tidy h
@@ -61,4 +75,50 @@ theorem computableInPolySpace_iff_computableTidilyInPolySpace :
     ComputableInPolySpace f encIn encOut ↔ ComputableTidilyInPolySpace f encIn encOut :=
   ⟨ComputableInPolySpace.tidy, ComputableInPolySpace.of_tidy⟩
 
+namespace ComputableInPolySpace
+
+variable {γ δ : Type} {encMid : β ↪ List Bool} {encD : δ ↪ List Bool}
+
+/-! ### Closure and automation -/
+
+/-- Polynomial time is within polynomial space. -/
+@[fun_prop]
+theorem of_polyTime (h : ComputableInPolyTime f encIn encOut) :
+    ComputableInPolySpace f encIn encOut :=
+  .of_tidy (.of_polyTime h.tidy)
+
+/-- The identity. -/
+@[fun_prop]
+theorem id' : ComputableInPolySpace (fun a : α => a) encIn encIn :=
+  .of_tidy .id'
+
+/-- Composition. -/
+theorem comp {f : β → γ} {g : α → β} {encOut : γ ↪ List Bool}
+    (hf : ComputableInPolySpace f encMid encOut) (hg : ComputableInPolySpace g encIn encMid) :
+    ComputableInPolySpace (fun a => f (g a)) encIn encOut :=
+  .of_tidy (hf.tidy.comp hg.tidy)
+
+/-- Pairing. -/
+@[fun_prop]
+theorem prod {g : α → δ} (hf : ComputableInPolySpace f encIn encOut)
+    (hg : ComputableInPolySpace g encIn encD) :
+    ComputableInPolySpace (fun a => (f a, g a)) encIn (encPair encOut encD) :=
+  .of_tidy (hf.tidy.prod hg.tidy)
+
+/-- Case distinction. -/
+@[fun_prop]
+theorem ite {c : α → Bool} {g : α → β} (hc : ComputableInPolySpace c encIn encBool)
+    (hf : ComputableInPolySpace f encIn encOut) (hg : ComputableInPolySpace g encIn encOut) :
+    ComputableInPolySpace (fun a => if c a then f a else g a) encIn encOut :=
+  .of_tidy (hc.tidy.ite hf.tidy hg.tidy)
+
+/-- Composition, in the form used by `fun_prop`. -/
+@[fun_prop]
+theorem comp' {f : β → γ} {g : α → β} {encOut : γ ↪ List Bool}
+    (hf : ComputableInPolySpace f encMid encOut) (hg : ComputableInPolySpace g encIn encMid) :
+    ComputableInPolySpace (fun a => f (g a)) encIn encOut :=
+  hf.comp hg
+
+end ComputableInPolySpace
+
 end Turing.MultiTapeTM
diff --git a/ComplexityTests/ResourceBoundsPlain.lean b/ComplexityTests/ResourceBoundsPlain.lean
index 71573c6b67..5a6d4afa1f 100644
--- a/ComplexityTests/ResourceBoundsPlain.lean
+++ b/ComplexityTests/ResourceBoundsPlain.lean
@@ -89,6 +89,33 @@ theorem id_computableInPolySpace :
 example : ComputableTidilyInPolySpace (id : List Bool → List Bool) encBits encBits :=
   id_computableInPolySpace.tidy
 
+/-! ### Compositional automation within plain polynomial space -/
+
+example {α : Type} (enc : α ↪ List Bool) :
+    ComputableInPolySpace (id : α → α) enc enc := by
+  fun_prop
+
+/-- Compose functions with plain certificates without converting either hypothesis by hand. -/
+example {α β γ : Type} {encA : α ↪ List Bool} {encB : β ↪ List Bool}
+    {encC : γ ↪ List Bool} {f : α → β} {g : β → γ}
+    (hf : ComputableInPolySpace f encA encB) (hg : ComputableInPolySpace g encB encC) :
+    ComputableInPolySpace (fun a => g (f a)) encA encC := by
+  fun_prop
+
+/-- Pairing and case distinction can mix plain space, tidy space and plain time certificates. -/
+example {α β γ : Type} {encA : α ↪ List Bool} {encB : β ↪ List Bool}
+    {encC : γ ↪ List Bool} {f : α → β} {g h : α → γ} {c : α → Bool}
+    (hf : ComputableInPolySpace f encA encB) (hg : ComputableTidilyInPolySpace g encA encC)
+    (hh : ComputableInPolyTime h encA encC) (hc : ComputableInPolyTime c encA encBool) :
+    ComputableInPolySpace (fun a => if c a then (f a, g a) else (f a, h a))
+      encA (encPair encB encC) := by
+  fun_prop
+
+/-- Missing certificates fail instead of cycling between the plain and tidy predicates. -/
+example {f : List Bool → Bool} : f = f := by
+  fail_if_success have : ComputableInPolySpace f encBits encBool := by fun_prop
+  rfl
+
 /-- The copy machine computes the identity in fpt time, for every parameter. -/
 theorem id_computableInFPTTime (κ : List Bool → ℕ) :
     ComputableInFPTTime (id : List Bool → List Bool) encBits encBits κ :=
@@ -158,6 +185,14 @@ example : ∃ f, ComputableInPolySpace f encQBF encBool ∧ ∀ φ, φ ∈ TQBF
   obtain ⟨f, hf, hA⟩ := mem_PSPACE_iff_computableTidilyInPolySpace.mp TQBF_mem_PSPACE
   exact ⟨f, .of_tidy hf, hA⟩
 
+/-- A plain polynomial-time preprocessing of the existing TQBF decider stays in `PSPACE`.
+The decider's tidy certificate and the preprocessing's plain certificate compose automatically. -/
+example {α : Type} {enc : α ↪ List Bool} {f : α → Logic.PL.QBF ℕ}
+    (hf : ComputableInPolyTime f enc encQBF) : {a | f a ∈ TQBF} ∈ PSPACE enc := by
+  obtain ⟨dec, hdec, hA⟩ := mem_PSPACE_iff_computableTidilyInPolySpace.mp TQBF_mem_PSPACE
+  have hcomp : ComputableInPolySpace (fun a => dec (f a)) enc encBool := by fun_prop
+  exact mem_PSPACE_iff_computableTidilyInPolySpace.mpr ⟨_, hcomp.tidy, fun a => hA (f a)⟩
+
 /-- `SAT` has a plain fpt-time decider in the number of variables. -/
 example : ∃ g, ComputableInFPTTime g encCNF encBool Logic.PL.CNF.numVars ∧
     ∀ φ, φ ∈ SAT ↔ g φ = true := by