Proposed addition: Mathlib.Computability.RecursionTheorems

Stream: new members

[Richard Zandi]

Wraps Nat.Partrec.Code.fixed_point into the full Second Recursion Theorem (kleene_fix₂) and provides a reusable diagonal gadget (Flipper) that immediately yields Gödel/Turing/Rice-style impossibility results. 100 LOC, zero sorrys. Would maintainers be happy with a PR along these lines?

[Bjørn Kjos-Hanssen]

(I'm not a maintainer but) I think people are generally happy to review PRs that contain proofs of important fundamental theorems that are not yet in Mathlib.