Mathlib TuringDegree uses partial oracles: Spector minimal degrees are not atoms there

Mathlib's TuringDegree is the antisymmetrization of TuringReducible on all partial functions ℕ →. ℕ, and a query to Nat.RecursiveIn.oracle at an undefined point diverges. Because of this, classical theorems about degrees of sets can become false when stated naively with TuringDegree. Example: for any set A, the partial function D = (0 on A, undefined off A) satisfies D ≤ᵀ charFun A. Every convergent computation from D gets only the answer 0, so it is also a computation from the constant-0 oracle. Hence every total f ≤ᵀ D is computable (proof: induction on Nat.RecursiveIn; each constructor is graph-monotone, including rfind via Nat.mem_rfind), while D is partial recursive iff A is c.e. So no noncomputable set's degree is an atom of Mathlib's TuringDegree, even though Spector minimal degrees exist among total degrees. State minimality for total D (∀ x, (D x).Dom).