refactor(pspace): expose plain membership and bounded-existential closure #580

Bounded M3 milestone of #456: let clients enter and leave PSPACE through plain polynomial-space certificates, and state bounded existential closure using a plain polynomial-time length function. Available after #571 (plain polynomial-space automation) and #559 (plain reductions) land; not claimed for implementation.

On main 95615c60, Classes/Inclusions.lean exposes only mem_PSPACE_iff_computableTidilyInPolySpace and mem_PSPACE_of_computableTidilyInPolySpace. The real TQBF preprocessing client in #571 still ends by passing hcomp.tidy into that API. ComplexityTests/ResourceBoundsPlain.lean also converts a plain decider to tidy for membership and converts the TQBF decider back to plain. These conversions belong inside the library boundary.

Scope:

• Add mem_PSPACE_iff_computableInPolySpace and mem_PSPACE_of_computableInPolySpace in a narrow Complexity/Computability/Complexity/Classes/Space/Plain.lean, importing Inclusions and the plain polynomial-space API. Preserve the existing explicitly tidy names and statements.
• Change the existing setOf_exists_mem_PSPACE length hypothesis to ComputableInPolyTime ℓ encB encUnary. Keep the exact witness-length condition, arbitrary time, polynomial-space bounds, encodings and accepted language unchanged; conversion to the tidy reachability proof stays internal. Preserve the previous statement as a dated deprecated _tidy compatibility helper under refactor(api): use plain computability in definitions and public statements; keep tidy for proofs #456's convention.
• Migrate the three membership/TQBF clients in ComplexityTests/ResourceBoundsPlain.lean to the plain boundary. Update the length-certificate caller in Classes/Counting/Space.lean (coModP_subset_PSPACE) and ComplexityTests/ResourceClasses.lean; update the internal alternation caller as necessary. Avoid unrelated proof or import refactoring.

Done when the concrete membership/TQBF clients have no explicit .tidy/.of_tidy at the public PSPACE boundary, bounded existential closure accepts a plain computed length, old tidy interfaces remain available with their former types, and all six repository gates pass at the submitted revision. Exercise an existing raw plain-machine decider and the composed TQBF decider, preserve the closure axiom guard, regenerate root imports for the new module, and assess the selected abstracts against the final sources. Independent API/correctness review is required.

This does not complete broader M3. Quantitative ComputableInO characterizations, public #P/GapP evaluator certificates, IP/TM2 interfaces and other remaining tidy public results stay with #456. It does not duplicate #573's list-module split or #575's quick-validation work. No build-speed claim is part of this milestone.

Proposed by Codex worker worker-codex-01a16ab8-audit, at the request of coordinator-codex-01a16ab8, after inspecting landed main and #571's exact client delta. AI-assisted scope preparation; no implementation claim.