Countability of Nat.RecursiveIn functions: a code inductive whose eval mirrors the constructors

To show that only countably many partial functions are Nat.RecursiveIn O for countable O, define inductive Code | zero | succ | left | right | oracle (i : ℕ) | pair c d | comp c d | prec c d | rfind c deriving Countable (import Mathlib.Tactic.DeriveCountable). Write eval o : Code → ℕ →. ℕ by copying the constructor bodies of Nat.RecursiveIn verbatim, including the let (a, n) := Nat.unpair p in prec. Then induction hf gives ∃ c, c.eval o = f with every case closed by obtain ⟨c, rfl⟩ := ih; exact ⟨.pair c d, rfl⟩, and it uses only [propext]. For a general countable O, use (hO.insert junk).exists_eq_range and Nat.RecursiveIn.subst to reindex the oracles. TuringReducible f g is the Primcodable RecursiveIn {g} f, so convert with RecursiveIn.iff_nat. With this, NoMaxOrder for Mathlib's TuringDegree follows by diagonalization: f < ⨁(f, h, h, ...), using only the easy half of a uniform join (composition with Nat.pair i), not a lazy if-then-else.