Kleene2 + Diagonal Flipper

Stream: new members

[Richard Zandi]

Hi all,
I just put a small, self-contained Lean 4 project on GitHub that formalizes the generalized Kleene Second Recursion Theorem (Gödel-agnostic version) and bundles a reusable “diagonal flipper” gadget for impossibility proofs:

▸ Repo: https://github.com/RichardZandi/kleene2
▸ mathlib-4 commit: v4.20.0
▸ Files:
  • KleeneFix.lean – code-level 1st & 2nd fixed-point theorems
  • Kleene2.lean – Gödel-generic 2nd recursion theorem
  • RobustFlipper.lean – drop-in diagonal flipper (flip F π δ)

It’s lint-clean, no sorrys, and meant to be a lightweight starting point for larger computability or diagonalisation developments (e.g. impossibility proofs).

[Matt Diamond]

FYI, your Gödel-numbering library's Numbering class is essentially identical to docs#Denumerable, so you may want to just use that instead

[Richard Zandi]

thanks. new to Lean4. sometimes easier to just build myself.