feat(api): register plain resource notions with fun_prop #556

Follow-up to #551 / #555 (M1b of #456). The design commitments say computability predicates are @[fun_prop]-registered. #554 does this for ComputableInPolyTime. The plain resource notions added in #555 are not registered yet, so a plain goal has to go through .tidy/.of_tidy by hand.

Scope

• In Complexity/Computability/Machines/Turing/MultiTape/Complexity/PolySpace/Plain.lean, mirroring refactor(api): add plain polynomial-time computability with tidy bridges #554's PolyTime/Plain.lean:
  • attribute [fun_prop] ComputableInPolySpace.
  • @[fun_prop] on ComputableTidilyInPolySpace.computableInPolySpace as the tidy-to-plain transition rule.
  • Plain closure rules proved through .tidy, matching the tidy set at PolySpace.lean:143 (of_polyTime, id', prod, ite, comp').
  • of_polyTime takes refactor(api): add plain polynomial-time computability with tidy bridges #554's ComputableInPolyTime.
• Optional, same pattern: ComputableInFPTTime in Parameterized.lean, with ite and composition along a parameter bound. ComputableInO/ComputableInSpace carry explicit bounds, so they are less natural fun_prop targets; register them only if a consumer needs it.

Consumers. These are the M3 restatements of polynomial-space results that build deciders compositionally today with tidy fun_prop/combinators:

• setOf_exists_mem_PSPACE, mem_PSPACE_iff_computableTidilyInPolySpace and PolyTimeReducible.mem_PSPACE (Classes/Inclusions.lean)
• Classes/Counting/Space.lean, Classes/SharpP/Space.lean
• Classes/IP/PSPACE.lean, Classes/IP/Simulation.lean
• Classes/Space/TM2.lean

Done when: a plain ComputableInPolySpace goal built from plain and tidy parts closes by fun_prop, with a test client, and the six gates pass.

Depends on #555 and #554.

Opened by worker-claude-551-c4b0c164 (Claude Code, Opus 5.5), delegated by coordinator-claude-c4b0c164-20261023, at the request of the #555 review.