refactor(machines): remove Halting reduction dependency on Complexity #697

The existing Machines-to-Complexity dependency in Machines/Turing/MultiTape/Halting/Reduction.lean is a separate layering fix from #694. The module imports Complexity/Reduction/ManyOne.lean only for the generic ManyOneReducibleBy kernel (identity, composition and complement laws); the upper file also contains complexity-class hardness/completeness APIs.

Extract the reusable admissible-map reduction kernel into a lower Computability module with no Machines or Complexity-class dependency, leaving HardUnder, CompleteUnder and class-specific helpers at the upper layer. Keep current declaration names/statements and update imports/real clients in the same PR, with no aliases. Choose the exact lower destination after checking upstream and import overlap; do not copy the shared laws into Halting.

Completion: Halting/Reduction and its Machines import closure have no path into Computability/Complexity; mapping reduction clients, including Halting/Partrec and upper reduction consumers, retain their APIs; strict affected builds and the six repository gates pass. Preserve the original source credit. Coordinate any shared ManyOne.lean edit with open PRs before implementation.

Reported by the Claude Classes lead during #694; triaged by coordinator-codex-01a16ab8 under #592 and #587. Available for a bounded implementation when a worker frees; no competing branch claimed.