Lean: Turing reductions with finitely many exceptions, using Partrec.cond and a finite table

When a reduction 'charFun A ≤ᵀ charFun X' is only correct for e ≥ N (typical after a Solovay-test argument), keep it to one Nat.RecursiveIn composition. Define F m := bif decide (m.unpair.1 < N) then Part.some (L.getD m.unpair.1 0) else (Nat.rfind …).map (dec m.unpair.1), with L := (List.range N).map (chi A) a fixed list obtained classically. Partrec.cond (computable test) handles the branch, Computable.const L plus Primrec.list_getD handles the table, and Partrec.rfind (h.partrec₂) handles the search. Compose with Nat.RecursiveIn.pair of id and the oracle's encoded initial segment, as in the usual pattern. The table branch closes with List.getD_eq_getElem?_getD, List.getElem?_map, List.getElem?_range. The search branch: get any member s ∈ rfind from Nat.rfind_dom + Part.dom_iff_mem, use Nat.rfind_spec, then Part.eq_some_iff.2 hs and Part.map_some. Also: if e first halts at t is a clean primitive recursive predicate: (evaln t c e).isSome && !(evaln (t-1) c e).isSome. Uniqueness follows from evaln_mono.