Making a classical finite-extension construction ∅′-computable: replace h.choose by Nat.find over ⟨ρ, steps⟩ with evaln
If a stage is if h : ∃ ρ, (Code.eval c (input ρ)).Dom then ... h.choose ..., first make the choice canonical: convF m := Code.evaln m.unpair.2 c (input (decodeString m.unpair.1)) and if h : ∃ m, (convF m).isSome then ... Nat.find h .... The noneffective proof barely changes. Use Code.evaln_sound to get v ∈ eval from Option.get_mem. In the divergent case, Code.evaln_complete turns a membership into ⟨encode ρ, k⟩ with isSome. Afterwards, ∅′ computes the stages. The question ∃ m, isSome is Σ₁, so reduce it via REPred.exists_of_computable₂ plus a many-one reduction to the halting set. Then do one rfind whose test is b = 0 || isSome (convF m), where b is the oracle's answer, so it stops at m = 0 when the answer is no. That avoids needing a lazy if in Nat.RecursiveIn. Use Option.getD in the primrec output and prove getD = get under isSome. Gotcha when coding a relation on a Primcodable type into a set: use decode₂, not decode, because decode k = some a does not imply encode a = k. Encodable.mem_decode₂ gives the iff, and Primrec.decode₂ exists.
Name check (Mathlib v4.35.0 and v4.36.0-rc2):
REPred.exists_of_computable₂is not in Mathlib. The onlyREPred.*lemma there isREPred.of_eq(Computability/RE.lean), so if this is your own helper, please mark it as such. The rest exists as used:Code.evaln_sound,Code.evaln_complete(an iff,x ∈ c.eval n ↔ ∃ k, x ∈ evaln k c n),Encodable.mem_decode₂,Primrec.decode₂. The decode₂ gotcha is real. A concrete case:decode (α := Finset ℕ) (encode [1, 0])issome {1, 0}withencode [1, 0] = 4, butencode ({0, 1} : Finset ℕ) = 10.