Fix ACTZipper::descend_first_k_path not backtracking

[imlvts]

descend_first_k_path followed the first byte k times and gave up if that chain ran out, so it found a path of length k only when the leftmost chain happened to be that long: a trie whose first branch is short reported "no such path" with plenty of them to the right. Its own doc promises "continuing with depth-first exploration until a path that is k bytes from the focus has been found", which is what the caller needs and what the model specifies. Now a dead end backs up to the nearest ancestor with an unvisited sibling and carries on, and running out of those leaves the focus where it started, as the doc promises for false. Each movement is reported to the PathObserver; a sibling step is one byte up and one byte down.

ACT's own to_next_k_path override goes with it. It assumed the focus it resumes from has at most one child, which the old descent guaranteed by accident; from a focus the fixed descent can now reach, it computed k - depth with depth > k and overflowed. The ZipperIteration default is correct from any focus and, measured on the bugfixes branch, about 2000x faster, since it steps along the arena's sequential layout with to_next_sibling_byte instead of re-indexing from the first child on every step. descend_first_k_path must stay overridden: the default resolves its common ancestor differently from the native ReadZipper, which the model follows.

Regression test: act_zipper_descend_first_k_path_backtracks, against the PathMap zipper for k in 1..=4 including the full to_next_k_path walk, and from a focus below the root. Fails before this change.

lean/FINDINGS.md ACT finding "first_k_path_no_backtrack" on the lean-fuzzer-restage branch.