Lean: limit-computable path of a finite-path tree without oracle machinery

To prove 'X ≤ᵀ ∅′' for a path X of a tree T that has only finitely many paths (e.g. Chaitin's K-trivial ⇒ Δ⁰₂), you can avoid Mathlib's RecursiveIn oracle plumbing entirely. Build a computable *limit approximation* and apply a limit lemma (Shoenfield: computable a(s,n) with a(s,n) → X n eventually gives X ≤ᵀ ∅′). Inputs: a computable approximation A(s,σ) → [σ ∈ T] pointwise, and non-uniform constants: k = number of paths, a level L at which they are pairwise distinct, and X↾L. Guess for bit n at stage s: with m = n+1, take the least j < s such that exactly k strings of length m have an extension by j bits in A(s,·). Output bit n of the one extending X↾L. Correctness: the true counts are ≥ k for every j (the paths' restrictions). By weak Kőnig applied to {ρ ∈ T | ρ comparable with σ}, every non-path string of length m dies at some depth. So some depth has count exactly k, and at the least such depth j* the survivors are exactly the path restrictions (Finset.eq_of_subset_of_card_le). Once A has stabilized on strings of length ≤ m + j* and s > j*, the stage search sees the true counts for all i ≤ j*, so it finds j*. Stabilization on a finite set: choose t ht using hlim, then take the Finset.sup of t. Lean gotchas: (1) after set L := F.sup w, simpa [w, h] using Finset.le_sup ... unfolds L into an existential. Use obtain ⟨L, hL⟩ : ∃ L, L = F.sup w := ⟨_, rfl⟩ and rw [← hL] at this. (2) Mathlib has no Computable.list_map. Build restrict X n by Computable.nat_rec with l ++ [X k] and prove equality by induction. (3) Primrec.list_getD takes the default as an explicit argument: (Primrec.list_getD false).