[SamuelSchlesinger]

Change

PSPACE now has the same shape as P and L:

def PSPACE (enc : α ↪ List Bool) : Set (Set α) :=
  {A | ∃ f : α → Bool, ComputableInPolySpace f enc encBool ∧ ∀ a, a ∈ A ↔ f a = true}

mem_PSPACE is Iff.rfl, like mem_P. Before, PSPACE spelled out the time/space pair ∃ t s, PolyBounded … s ∧ ComputableInTimeAndSpace f enc encBool t s, while the closure proofs went through a separate bridge to ComputableInPolySpace. That bridge now holds by definition, so the two wrappers around it are deleted:

• mem_PSPACE_iff_computableInPolySpace, an exact duplicate of mem_PSPACE;
• mem_PSPACE_of_computableInPolySpace, its .mpr.

Their callers in nine files now build or destructure membership directly with ⟨f, hf, hA⟩, as callers of P do: the closure lemmas in Space/Closure, plus Counting/Space, IP/PSPACE, Space/TM2, SAT/Space, TM2/Reverse/Transfer and three tests. mem_PSPACE_iff, the bridge to upstream DecidableInTimeAndSpace, is unchanged in statement.

Three proofs built membership from an explicit time/space bound: Savitch's mem_PSPACE_of_recognizesInSpace, TQBF_mem_PSPACE and mem_PSPACE_iff. They now share one constructor, mem_PSPACE_of_computableInTimeAndSpace, which goes through ComputableInPolySpace.of_inSpace. P_subset_PSPACE becomes ⟨f, .of_polyTime hf, hA⟩. L_subset_PSPACE becomes L_subset_P.trans P_subset_PSPACE, the only edit to LogSpace.lean and clear of #4800's hunks. The ComputableInO characterization in Space/Closure now uses of_inSpace instead of rebuilding the polynomial bound.

This is refactoring only, with no new mathematics. The definition is equivalent to the old one: a Boolean output has length one, so ComputableInPolySpace's output charge is free. Net −14 lines (+71/−85).

Imports: Space.lean gains public import …MultiTape.ResourceBounds for the definition. That module was already in its transitive closure, so no new fan-out. It also gains a private import …Complexity.PolySpace.Plain for of_polyTime / of_inSpace. This adds four small modules to Space's build closure (PolySpace, PolySpace.Plain, BigO.Plain, InSpace.Plain). Space/Closure, Oracle/Space and most other PSPACE clients already import them.

Manual impact

Operator's Manual: no edit. manual/machines-and-classes/native-and-resources.md lists PSPACE among the classes that "derive familiar bound families" and describes ComputableInPolySpace in its resource table. Both are still accurate, and no chapter names the removed lemmas (git grep). Agent Operator's Manual: no edit, since no workflow or tooling changed. ROADMAP.md, results/README.md, CslibFrontierResults/ and TM2/README.md do not name the removed declarations or describe PSPACE's body.

Validation

At 7eddd80 (based on main 936b94e; git merge-tree with main d3c8831 is clean, and main has not touched these files since the base):

• lake build --wfail --iofail on every library, test and results module that mentions PSPACE (85 modules, including all changed files and the destructuring clients Savitch, TQBF, EXPSPACE, Oracle/Space, Inclusions, Alternation and TM2/Reverse/Transfer).
• lake exe mk_all --check, python3 -B scripts/check_operator_manual.py, check_hygiene.py --check-simp, and both ratchets (check_encoding_readability.py, check_projection_chains.py).
• python3 scripts/proof_copies.py --base origin/main: no repeated proof block.
• python3 scripts/parallel_defs.py --theorems --no-build-check: no duplicate among the 19 theorems. Coverage is partial because 11 unrelated library modules had no local build outputs.

Full validation is left to CI.

AI assistance

Jetski worker session c0af227b, plan #4737. Agent-written; not yet reviewed by a human.

Part of #4737

[SamuelSchlesinger]

Agent review (Jetski reviewer session aa3000d8-52c2-410f-8f18-9f617338b54e) of 7eddd80: approve. This is agent review, not human review.

The refactor holds up. PSPACE now has the same shape as P and L: ∃ f, Computable… f enc encBool ∧ ∀ a, a ∈ A ↔ f a = true. mem_PSPACE is Iff.rfl, like mem_P. The new definition is equivalent to the old one: ComputableInPolySpace's output charge (encBool (f a)).length ≤ s n costs nothing, because of_inSpace builds c * (b n + 1) ≥ 1. Removing mem_PSPACE_iff_computableInPolySpace (now mem_PSPACE by definition) and its .mpr takes nothing away. All in-repo clients are updated, with no aliases:

• git grep finds neither name anywhere at the head, including manual/, results/, CslibFrontierResults/ and TM2/README.md.
• Every use on current main lies in a file this PR edits.

API:

• mem_PSPACE_of_computableInTimeAndSpace is a natural constructor. Its explicit t s : α → ℕ match ComputableInTimeAndSpace, and the name parallels mem_PSPACE_of_computableInO in Oracle/Space. It has three real clients: Savitch, TQBF_mem_PSPACE and mem_PSPACE_iff. Each previously built the old tuple by hand.
• P_subset_PSPACE is now ⟨f, .of_polyTime hf, hA⟩.
• L_subset_PSPACE is now L_subset_P.trans P_subset_PSPACE.
• The reverse direction of mem_PSPACE_iff_computableInO now goes through of_inSpace instead of rebuilding the polynomial bound.

Each of these reads better. The anonymous-constructor clients match how P membership is written.

Imports: the public ResourceBounds import adds nothing to the closure; it was already transitive. The private PolySpace.Plain import adds four modules (PolySpace, PolySpace.Plain, BigO.Plain, InSpace.Plain, about 640 lines) to Space's build closure. It changes no public interface. I checked the import graph at the base: 89 of Space's 218 transitive dependents, and 10 of its 15 direct importers, already import PolySpace.Plain. That is acceptable.

Non-blocking follow-up: of_polyTime and of_inSpace need only ResourceBounds, PolyTime and InSpace.Plain, which Space already imports. If a later change moves them to a small PolySpace/Basic module, Space could drop the import.

Manuals: I agree no edit is needed. manual/machines-and-classes/native-and-resources.md still describes PSPACE and ComputableInPolySpace correctly. The Agent Operator's Manual is unaffected. ROADMAP.md and the results inventory name neither removed declaration.

Open PRs:

• The only textual overlap is refactor(Complexity/LogSpace): LogSpaceComplete.mem_L_iff and its three clients #4800 (LogSpace.lean); git merge-tree is clean.
• refactor(Complexity/Problems): migrate cycles, games, and drawings to structures (#4385) #4672 already conflicts with main in CslibFrontierTests/InteractiveProofs.lean and elsewhere. When it merges main, it should keep this PR's anonymous constructor.
• feat(Complexity): parameter-sensitive reductions, DFS batching, and word-oracle transfer #4530 (conflicting, changes requested) ends BoundedOracleReduction.mem_PSPACE with the old tuple shape ⟨_, ⟨T_A, …, htm_A⟩, _⟩. After this lands, the exists_inSpace unpacking should collapse to something like ⟨_, hf_ps, fun _ => by simp⟩. It is a one-line adjustment when feat(Complexity): parameter-sensitive reductions, DFS batching, and word-oracle transfer #4530 next merges main.
• No other open PR uses the removed names.

Other reviews: none on this PR at the time of review, so there are no open findings.

CI at this head: ci-checks and guide pass. Advisory notices:

• No repeated proof block (131 proofs).
• No parallel definition.
• No duplicate statement (19 theorems).
• PR description names: flags only the two removed declarations, which the description names deliberately as deleted.