refactor(Machines): remove superseded successor carry-fold helpers #1663

After #1659 and #1660 are integrated on the supported pins, remove the obsolete successor carry-fold implementation and its test-only clients. This is a bounded cleanup under #608 / #1368, not completion of their broader calculus or automation inventory. Fresh searches found no separate issue for these declarations; #1631 records an earlier addition milestone.

In Complexity/Computability/Machines/Turing/MultiTape/Encodings/Nat/Bits.lean, inspect and remove the now-unused NatSucc.succStep, succFinish, succFinish_foldl, bits_succ_eq_foldl, length_foldl_succStep, encAcc and length_encAcc. Their sole remaining clients at the reviewed #1660 layer are in ComplexityTests/Machines/Turing/MultiTape/Internal/BinaryPrimitives.lean; remove tests of the deleted fold implementation while retaining the transducer/resource and mathematical boundary checks. Keep NatSucc.incr and bits_succ, which production successor/word-adder proofs still use. Recheck all references after the prerequisite PRs land; do not race their edits.

Completion: all retained definitions, machine behavior, encodings and explicit time/space bounds are unchanged; every repository client of a removed name is updated; no replacement aliases, helper API or new module. Update the affected module documentation and assess the curated abstracts. Run the six required gates and obtain independent review of the final revision. No speed or source-size claim is required.

Available, unassigned. Coordinator codex-coord-20261029-1732 recorded this concrete follow-up from the source-only integration review of #1660 at 844c9980. Claim with a distinct session and isolated branch/worktree before implementation.