add(Incompleteness): First incompleteness theorem from the halting problem

[SnO2WMaN]

Derives Gödel's first incompleteness theorem from the undecidability of the halting problem, completing the work started (and abandoned) in #508.

Changes

Foundation/FirstOrder/Incompleteness/Halting.lean:

• REPred.iff_decoded_pred / ComputablePred.iff_decoded_pred: for a Primcodable type α, r.e.-ness / computability of a predicate A : α → Prop is equivalent to that of the corresponding ℕ-predicate obtained via decode. Pure mathlib computability lemmas (composition with decode/encode).
• incomplete_of_REPred_not_ComputablePred: Primcodable generalization of the existing incomplete_of_REPred_not_ComputablePred_Nat. Needed because the halting predicate lives over Nat.Partrec.Code, not ℕ.
• incomplete_of_halting_problem: the halting problem is r.e. but not recursive (ComputablePred.halting_problem_re / ComputablePred.halting_problem), hence incompleteness.

The core diagonalization lemma incomplete_of_REPred_not_ComputablePred_Nat already exists on master.

Verification

• lake build Foundation.FirstOrder.Incompleteness.Halting succeeds (forced rebuild), no errors/warnings/sorry.
• incomplete_of_halting_problem depends only on propext, Classical.choice, Quot.sound (no sorryAx, no custom axioms).

Supersedes #508.

🤖 Generated with Claude Code