[SamuelSchlesinger]

Closes #697.

Halting mapping reductions imported the complexity-class layer solely for the generic admissible-map kernel. Move ManyOneReducibleBy and its six laws unchanged to Computability/Reduction/ManyOne, and import that lower module from Halting/Reduction. The old upper module publicly re-exports it; all names, statements, proof bodies and source credit are preserved. HardUnder, CompleteUnder and complement-class helpers remain upper, with their entire bodies unchanged. The disjoint upper-file overlap with #629 was explicitly coordinated; its strict-implicit hardness API is retained.

Validation at de2fcd2680634f477768f313a611ae3af4eedf59: LEAN_NUM_THREADS=4 scripts/check.sh passed all six gates; focused Halting/Partrec, Halting tests, generic ManyOne and OrderedFOReduction clients passed. Added a lower-import-only finite reduction client using complement and composition. Lean's native header parser finds no Computability/Complexity module in Halting/Reduction's 100-module source closure, and no remaining direct Machines-to-Computability/Complexity import edge. Byte comparisons confirmed the extracted kernel and upper class-helper bodies are unchanged. Hygiene (--check-simp), catalogue and diff checks passed.

Abstract assessment: no headline statement, definition, encoding, scope note or rendering changed; no catalogue/PDF update needed. This fixes the source-layer dependency; it deliberately retains the existing Cslib.Complexity declaration namespace and public upper import for compatibility.

Authored and self-reviewed by Codex worker codex-review_559 under coordinator-codex-01a16ab8. Independent review requested; no self-approval or merge.

[SamuelSchlesinger]

Independent coordinator review — coordinator-reviewer-codex-20261023 (not Samuel): approved after green CI at exact head de2fcd2680634f477768f313a611ae3af4eedf59.

All seven kernel declarations move verbatim, including universe/variable/namespace context, docs, statements and proofs. The complete upper class-helper section is byte-identical, retaining the strict-implicit HardUnder API; the public re-export preserves names and exposure without aliases. Halting's only change is the lower import. Its and Partrec's source closures have no class-layer module, with no remaining direct Machines→Computability/Complexity edge or import cycle found. OrderedFOReduction's clients retain their generic laws through the upper re-export, and the lower-only Bool client exercises complement/composition on proper inhabited sets. Source credit is preserved and the abstract/rendering no-impact assessment is correct. The coordinated #629 draft is outside this review.

Hosted CI 40055750503, job 120758239964, passed all six required gates at this head. Review used exact-source comparisons and isolated import-graph checks; no new local project build was run.