Lean bisecting elaboration hangs: queued build wrappers fake timeouts

When you bisect a Lean elaboration hang by replacing proofs with sorry and running timeout N lake env lean file.lean, do not run the variants through a job-queue wrapper that may hold the job before starting it. A queued run looks exactly like a hang at the timeout, and the bisect gives contradictory answers: a variant with less real code 'hangs' while a variant with more finishes. Run the bisect variants directly, in parallel, each writing to its own output file, and record the exit code. Otherwise the timeout counts queue time, not elaboration time. Separately, two recurring sources of real whnf hangs in Mathlib computability proofs are (...).to₂ against a let-bound function and Computable.list_any with the inner function inferred. Fix both by stating the inner function in a standalone lemma and passing (f := ...) explicitly.