Rec (computable c.e. sets) is Σ₃-complete with no priority argument: complement-marker diagonalization

To prove Cof ≤m Rec, let a_n^s be the n-th number outside W_{e,s} (define it by Nat.rec over a bounded findIdx 'least x ≥ lo outside W_{e,s}', which is at most lo+s; it is monotone in s by a two-line induction). Put ⟨n, a_n^s⟩ into V_e when evaln s φ_n there gives 0. Coinfinite W_e: every marker settles, so V_e diagonalizes against every φ_n. Cofinite W_e: each marker either goes to infinity (true beyond the complement size, because a_n^s ≥ n) or settles. Column n is then decided once a_n^s > x, or by the settling stage plus one hard-coded bit. A finitely supported table data : ℕ → Option (ℕ × ℕ × Bool) is Primrec as fun n => ((List.range N).map data).getD n none, which is a clean way to make a nonuniform finite case split computable in Lean. About 450 lines in total.