[SamuelSchlesinger]

Change

This refactors the Complexity reduction modules (lane reductions of #4737). It adds no new result, and no statement changes.

• polyTimeReducible_of_mem_P moves to its own module, Reduction/Nontrivial.lean. The lemma says that every problem in P reduces to every problem with a member and a nonmember. It lived in the Berman–Hartmanis conjecture module, so Classes/Ladner/Density.lean had to import the Cook–Levin and SAT padding machinery to use it. The new module imports only Reduction, and Density now imports it. I kept the name: the hypothesis is A ∈ P encA, so dot notation would not apply to a PolyTimeReducible.of_mem_P either.
• Oracle substitution moves to Classes/Oracle/Substitution.lean. These are ComputableInPolyTimeWithOracle.of_mem_PWithOracle, PWithOracle_subset_of_mem_PWithOracle and NPWithOracle_subset_of_mem_PWithOracle (O₁ ∈ P^{O₂} gives P^{O₁} ⊆ P^{O₂} and NP^{O₁} ⊆ NP^{O₂}), plus their private simulation step. They are statements about oracle classes, and they lived in Reduction/Turing.lean. The new module does not import Classes/Oracle/Lowness.lean. Turing.lean imports it publicly and uses it for PolyTimeTuringReducible.mem_PWithOracle and .trans, so its importers see the same declarations. The moved block is verbatim. The module docstring points to the many-one special case PolyTimeReducible.PWithOracle_subset in Classes/Oracle/Monotone.lean. That module proves its case independently and covers non-Boolean outputs, so I left it alone. Turing.lean's now-unused Polynomial.Automation import is dropped.
• The three restricted one-one reducibilities in Reduction/Isomorphism.lean get _iff_manyOneReducibleBy bridges, as PolyTimeOneOneReducible already has. The variants are invertible, length-increasing, and invertible length-increasing. Each bridge is Iff.rfl. The bridges record that each variant is definitionally a ManyOneReducibleBy instance, and they let clients state and rewrite with that API; no proof in this PR uses them. Independently, the variants' refl, trans, compl and five forgetful projections now apply ManyOneReducibleBy.refl/trans/compl/mono directly through that definitional equality, instead of hand obtain/refine proofs. Only the facts specific to each variant remain in these proofs: left inverses compose by hleft₂.comp hleft₁, and length increase is transitive.

Net lines: +298 / −208. Most of that is the move (about 145 lines of substitution and 11 of the lemma) plus the two new module docstrings. Isomorphism.lean is +54 / −43, and that includes the three bridge statements.

Manual impact

• Operator's Manual: no edit needed. reductions.md links Turing composition and closure in P at a pinned revision and describes them by meaning. It does not name the moved declarations or their modules, and the declarations keep their names and statements. The isomorphism table there names only the predicates, which are unchanged.
• Agent Operator's Manual: no edit needed, since roles, delegation and review are unchanged.
• ROADMAP.md, results/README.md and CslibFrontierResults/ do not name the moved declarations.

Validation

At d5e4481 (base 3d814ebfa5; main has not touched these files since):

• scripts/check.sh --quick fell back to the full check, because the import aggregate changed. Every gate passed: lake build, lake test, lake lint, lint-style, mk_all --check, checkInitImports, source hygiene, the encoding and projection ratchets, documentation pins, the tidy statement ratchet, result registry references and changed-file lints.
• scripts/parallel_defs.py --theorems reports no duplicate statement among the 22 theorems examined. scripts/proof_copies.py reports no repeated proof block.
• No line is over 100 characters (checked by character count).

Part of #4737

AI assistance

Jetski worker session a924892d, plan #4737. There has been no independent review yet.

[SamuelSchlesinger]

Agent review (Jetski reviewer session 39f68e58) of d5e4481: approve. This is agent review, not human review.

• The moves are verbatim. I diffed the removed lines against the added ones. The substitution block matches line for line: the private oracleAnswerStep helpers, ComputableInPolyTimeWithOracle.of_mem_PWithOracle, PWithOracle_subset_of_mem_PWithOracle and NPWithOracle_subset_of_mem_PWithOracle. So does polyTimeReducible_of_mem_P. The only text change is "language" → "problem" in that lemma's docstring. No statement changes.
• Imports. The transitive import closure of Classes/Oracle/Substitution.lean contains neither Classes/Oracle/Lowness nor Reduction/Turing. That of Reduction/Nontrivial.lean reaches neither Cook–Levin nor SAT, so Ladner/Density.lean no longer pulls in the Berman–Hartmanis machinery. Turing.lean re-exports Substitution publicly, so its importers keep the names. feat(Complexity): bounded-width CNF counting encodings and #2-SAT #P-completeness #4515's new CountingTuring.lean is one such importer.
• Open PRs. No other open PR adds a use of a moved or changed name; I scanned every open diff. perf(PolyTime): make ComputableInPolyTime irreducible #4150 (draft) edits only Oracle/Lowness.lean. feat(Complexity): parameter-sensitive reductions, DFS batching, and word-oracle transfer #4530 and feat(Complexity): bounded-width CNF counting encodings and #2-SAT #P-completeness #4515 do not touch these files. refactor(Complexity/NP): public NP guard and check lemmas, guarded reductions #4750 edits Density.lean away from the changed import line, so the two do not conflict textually.
• Names and docstrings. Reduction/Nontrivial.lean is a good name: the module is about reductions to nontrivial problems. Its docstring states the lemma and the P = NP consequence correctly. The Substitution docstring describes the simulation and points to the many-one special case in Oracle/Monotone.lean.
• Isomorphism. The three variants' refl, trans, compl and forgetful projections now go through ManyOneReducibleBy. Only the facts specific to each variant remain: left inverses compose, and length increase is transitive. Non-blocking: no proof references the three _iff_manyOneReducibleBy bridges, since the proofs elaborate by unfolding. So the bridges serve as stated characterizations. That matches the existing polyTimeOneOneReducible_iff_manyOneReducibleBy, which is also unreferenced. "With the bridges, ..." in the description overstates their role a little.
• CI. ci-checks passed at this head. The advisory notices report no parallel definitions, no duplicate statements among the 22 theorems examined, and no repeated proof block. The one PR-name notice (PolyTimeReducible.of_mem_P) is the alternative that the description deliberately rejects.
• Manuals. I checked the manual-impact assessment. reductions.md describes these results by meaning, at pinned revisions, and the Agent Operator's Manual is unaffected. No edit is needed.