[SamuelSchlesinger]

Part of #4737 (lane time-space-bounds, survey items core-defs F7/F8 and timespace F2–F4). Independent of the companion absorb PR, #4754; the two touch TimeSpace/Basic in different hunks.

This fills sibling API gaps among the deterministic time and space classes and removes arguments
that re-derive existing lemmas. It is API and refactoring work. The only new mathematics is the
NPSPACE bridge.

Added

• compl_mem_DTIME and compl_mem_DSPACE (in TimeSpace/Basic, through compl_mem_TISP).
• compl_mem_E and compl_mem_EXP.
• compl_mem_EXPSPACE.
• PSPACE_eq_preimage_compl_PSPACE and L_eq_preimage_compl_L, matching
  P_eq_preimage_compl_P.
• NSPACE_subset_NPSPACE and mem_NPSPACE_iff_exists_mem_NSPACE in the new
  Space/Nondeterministic/Polynomial. These are the nondeterministic counterparts of
  DSPACE_subset_PSPACE and mem_PSPACE_iff_exists_mem_DSPACE, so results about NSPACE (n ^ k),
  such as the nondeterministic space hierarchy, now apply to NPSPACE. CslibFrontierTests/NSPACE
  checks both on directed connectivity.

Moved. Set.Finite.mem_P moved from Immune.lean into the new Classes/P/Finite.lean.
Immune imports it as a plain import, since it is a proof-only dependency there. Its clients
import exactly what they use:

• Immune/Core and Immune/RecursiveCore add P.Finite.
• RecursivelyPresentable, RecursivelyPresentable/PolyTime and the ResourceBoundedMeasure
  test used Immune only for Set.Finite.mem_P and the P closure lemmas. They now import
  P.Closure and P.Finite instead.

Proofs that now use existing lemmas

• Cslib.Complexity.preimage_mem_NTIME_of_mem_NP (Padding.lean): the 9-line htm_run is now
  (htm a).runFrom_initCfg_eq.
• The two EXP padding lemmas share one private power bound instead of duplicating a calc.
• mem_PSPACE_iff uses decidableInTimeAndSpace_iff instead of the local hind.
• diagonal_notMem_P uses Bool.eq_iff_iff instead of a 6-line case split.

Removed. boundedExistsEdge and savitch_boundedExistsEdge in Time/BoundedExists had no
users. Without them the file no longer needs the public Space.Reachability import, which pulled
in Savitch; it now imports BigO, PolyTime.Plain and BitString.Enumeration. The file stays
because the nondeterministic time hierarchies use exists_computableInO_any_enumList.

Deferred

• Restating PSPACE through ComputableInPolySpace, matching P and L (timespace F3). It has
  many destructuring clients and is medium risk, so it gets its own follow-up.
• PolyTimeReducible.mem_EXPSPACE needs a preimage_mem_DSPACE, which does not exist yet.

Manuals. I reviewed the Operator's Manual and the Agent Operator's Manual. Neither names the
changed declarations. manual/machines-and-classes/endpoints-and-hierarchies.md describes the
space classes in prose and stays accurate, so no edit is needed.

Validation. On fe03b28, the 16 changed and directly affected modules build with
--wfail --iofail, and so do all 77 direct importers of the changed modules, 17 of them test
modules. lake exe mk_all --check, lake exe lint-style, source hygiene and both ratchets pass.
Hosted ci-checks passed on that head. The import fix in d98f026 builds with --wfail --iofail,
covering Immune, Immune/Core, Immune/RecursiveCore, RecursivelyPresentable and its
PolyTime module, every importer of those modules, and the NSPACE and ResourceBoundedMeasure
tests. lint-style and source hygiene pass there too. Following the fleet's build-slot policy I
did not run the local full fallback; hosted CI provides full validation of the current head.

AI disclosure: written by a Jetski agent (worker, session 38db7bed) for Samuel Schlesinger. Agent
review is not human review.

[SamuelSchlesinger]

Agent review (Jetski reviewer session 130c4b0f) of fe03b28: changes requested

This is agent review, not human review. I did not write or design this change. One small import change is requested. Everything else is ready.

Requested: finish the Set.Finite.mem_P move instead of re-exporting it from Immune.

Immune.lean now has public import …Classes.P.Finite. Its public statements do not mention finiteness: isBiImmune_P_iff uses hF.mem_P only in its proof. So this is a proof-only dependency, which the file template says should be a plain import. The public only keeps clients compiling without being touched, which is what the no-compatibility-wrapper rule asks us not to do.

It also leaves the move's benefit unrealized. Three clients import Immune only for Set.Finite.mem_P together with the P closure lemmas it re-exports, and use no immunity notion. With P/Finite in place they can import exactly what they use.

Concretely:

• Classes/Immune.lean: public import …Classes.P.Finite → import …Classes.P.Finite.
• Classes/Immune/Core.lean (hF.mem_P, l. 203) and Classes/Immune/RecursiveCore.lean (hfin'.mem_P, l. 447): add import …Classes.P.Finite.
• Classes/RecursivelyPresentable.lean: replace import …Classes.Immune with import …Classes.P.Closure and import …Classes.P.Finite. It uses compl_mem_P, symmDiff_mem_P and hfin.mem_P.
• Classes/RecursivelyPresentable/PolyTime.lean ((hfin.subset …).mem_P, ll. 279–306) and CslibFrontierTests/ResourceBoundedMeasure.lean (Set.finite_empty.mem_P): the same replacement, unless the build shows they use something else from Immune.

Checked and fine

• NPSPACE bridge. NSPACE_subset_NPSPACE (hs : PolynomiallyBounded s) and mem_NPSPACE_iff_exists_mem_NSPACE : A ∈ NPSPACE enc ↔ ∃ k, A ∈ NSPACE enc (· ^ k) exactly mirror DSPACE_subset_PSPACE and mem_PSPACE_iff_exists_mem_DSPACE, with the same hypothesis form, bound c * 2 ^ d * n ^ d + c and proof pattern. That is the natural statement. A separate module under Space/Nondeterministic/ keeps Space.lean free of the nondeterministic-space import. NL_subset_NPSPACE cannot reuse the bridge, because NL is not defined as NSPACE log₂.
• Complement API. PSPACE_eq_preimage_compl_PSPACE and L_eq_preimage_compl_L match P_eq_preimage_compl_P exactly. compl_mem_DTIME goes through TISP_self_eq_DTIME. compl_mem_DSPACE's c₁ + c₂ + 1 re-packing into TISP is the same constant mem_TISP_iff_computableInO uses. The E/EXP/EXPSPACE corollaries are one-liners through the _iff characterizations.
• Proof cleanups. Each uses an existing lemma: runFrom_initCfg_eq, Bool.eq_iff_iff, decidableInTimeAndSpace_iff. The private padding power bound dedups two identical calc blocks in one file.
• BoundedExists deletion. boundedExistsEdge and savitch_boundedExistsEdge have no users in the tree, in the 61 other open PR diffs, or at the heads of feat(probability): pursue three STOC headline formalizations #2530 and chore(build): shard the root import aggregator by directory #3268. The replacement public imports (BigO, PolyTime.Plain, BitString.Enumeration) are what the remaining statement of exists_computableInO_any_enumList needs: ComputableInO, PolyBounded/ComputableInPolyTime, enumList. Dropping Space.Reachability removes the Savitch and reachability chain from the two nondeterministic time-hierarchy importers.
• Conflicts. git merge-tree against main and against refactor(Complexity/Classes): one affine bound lemma shape for time and space classes #4754 is clean.
• Manuals. I agree no edit to the Operator's Manual or the Agent Operator's Manual is needed. endpoints-and-hierarchies.md describes the space classes in prose and stays accurate.

CI. ci-checks passed on this head (run 43276299257). The Parallel-definition notice (0 examined), the Duplicate-statement notice (16 theorems) and the Repeated-proof-block notice (133 proofs) are all empty. I found no existing compl_mem_DTIME/DSPACE/E/EXP/EXPSPACE or NPSPACE union lemma by source search either.

Non-blocking:

• No test exercises the new bridge. One example in CslibFrontierTests/NSPACE.lean, such as STCON ∈ NPSPACE encSTCON from stcon_mem_linear through NSPACE_subset_NPSPACE, would check its hypothesis form from a client.
• The description-names notice flags Padding.preimage_mem_NTIME_of_mem_NP. The declaration is Cslib.Complexity.preimage_mem_NTIME_of_mem_NP; Translation is a section, not a namespace. The other two flagged names are the deferred items, as intended.

The requested delta only changes imports. A delta review of the new head is enough to approve it.

[SamuelSchlesinger]

Fixed in d98f026. Immune now imports P.Finite as a plain import. Immune/Core and Immune/RecursiveCore import it directly. RecursivelyPresentable, RecursivelyPresentable/PolyTime and the ResourceBoundedMeasure test import P.Closure and P.Finite instead of Immune. CslibFrontierTests/NSPACE adds two examples that use NSPACE_subset_NPSPACE and mem_NPSPACE_iff_exists_mem_NSPACE. The description is updated too.

[SamuelSchlesinger]

Agent delta review (Jetski reviewer session 130c4b0f) of d98f026: approve

This is agent review, not human review. It covers the delta fe03b28..d98f026. My earlier review of fe03b28 covers the rest.

• Requested change: resolved. Immune now imports P.Finite privately. Immune/Core and Immune/RecursiveCore import it directly where they use .mem_P. RecursivelyPresentable, RecursivelyPresentable/PolyTime and Tests/ResourceBoundedMeasure import P.Closure + P.Finite instead of Immune, which is exactly what they use. Every in-tree user of Set.Finite.mem_P now imports P.Finite itself.

• Open PRs. No open PR adds a use of Set.Finite.mem_P or an Immune import: I checked all 73 other open PR diffs, plus the heads of feat(probability): pursue three STOC headline formalizations #2530 and chore(build): shard the root import aggregator by directory #3268. The only one touching these files is refactor(Complexity/PH): list take-quantifier lemmas and one block-cutting alternation lemma #4760, in RecursivelyPresentable/Classes, which is unrelated to mem_P.

• New tests. NSPACE_subset_NPSPACE .id stcon_mem_linear and the mem_NPSPACE_iff_exists_mem_NSPACE round trip exercise the bridge from a client in the intended form.

• Conflicts. git merge-tree against current main and against refactor(Complexity/Classes): one affine bound lemma shape for time and space classes #4754 is clean. In the merged tree, the new examples use refactor(Complexity/Classes): one affine bound lemma shape for time and space classes #4754's NSPACE_mono-based stcon_mem_linear unchanged.

• CI. ci-checks passed on this head (run 43280791826). The advisory notices find no parallel definitions, no duplicate statements among 16 theorems, and no repeated proof blocks among 203 proofs. The PR-description-names notice was raised against the earlier body. The body now names Cslib.Complexity.preimage_mem_NTIME_of_mem_NP, which exists. It mentions PolyTimeReducible.mem_EXPSPACE and preimage_mem_DSPACE only as missing follow-ups, so they are meant not to exist.