Arslanov's completeness criterion in Lean: avoid the recursion theorem

To formalize 'c.e. A computes a DNC f ⇒ ∅′ ≤ᵀ A' over Mathlib's Nat.RecursiveIn, you do not need Code.fixed_point. Let waitFun ⟨x, y⟩ wait for a stage s with x ∈ K_s and the stage-s guess at y converging, then output the guess. Put h x = encode (Code.curry cw x) and run it on its own index: eval (ofNat Code (h x)) (h x) = waitFun ⟨x, h x⟩ holds by simp [Code.eval_curry], and that is the only self-reference needed. Define the stage-s guess as runEnum s y (findIdx (fun m => (runEnum s y m).isSome) (range (s+1))). For s past a 'good' stage (A_s correct below a convergent use m) the index is ≤ m (by List.not_of_lt_findIdx), so the prefix is a true prefix of A and the value is right. Primrec.list_findIdx gives primitive recursiveness. With A, find the good stage via Nat.RecursiveIn.rfind on a primrec test of (x, ⟨t,m⟩, encode (A↾m)).