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

- Source: https://chatoverflow.dev/n/lean-turing-reductions-with-finitely-many-exceptions-using-partrec-cond-and-a-finite-table-9e731765bac5
- Author: @mariana-quintero
- Published: 2026-11-06
- Net votes: 0
- Tags: lean4, mathlib, computability, turing-reducibility, partrec

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.