feat(Computability): semilattice instance on Turing degrees

[tannerduve]

This PR equips TuringDegree with a SemilatticeSup structure by introducing the Turing join, proving usual least-upper-bound properties, and lifting these to degrees (quotients). In support of this, it extends the existing RecursiveIn API with some lemmas used in the degree theory.

The main contribution is the SemilatticeSup instance on TuringDegree. We define the Turing join as follows

turingJoin (f g) : ℕ → ℕ   -- notation: f ⊕ g

and prove it is a least upper bound:

• left_le_join, right_le_join
• join_le
• monotonicity and congruence lemmas (join_mono, join_congr)

We lift this to degrees in TuringDegree.sup, TuringDegree.le_sup_left, TuringDegree.le_sup_right, and TuringDegree.sup_le

instance : SemilatticeSup TuringDegree

New additions to RecursiveIn.lean:

• liftPrim, liftPrimrec, RecursiveIn', ComputableIn, ComputableIn₂: Encodes partial/total functions between Primcodable types as ℕ →. ℕ, analogous to Partrec/Computable.

• of_eq, of_eq_tot, of_primrec, some, none, mono, subst: Standard closure properties for RecursiveIn.

• cond_const, cond_core_rfind, cond, ComputableIn.cond: Shows RecursiveIn is closed under conditionals when the guard is absolutely computable

• Nat.Partrec.recursiveIn, Computable.computableIn: Every partrec/computable function is recursive in any oracle set.

Small addition to Partrec

we add to Mathlib.Computability.Partrec a small helper def (Partrec.kronecker and related rfind lemmas) representing the function that returns 1 if its two (unpaired) arguments are equal, and 0 otherwise, which is used in the proof of cond

TODO

Some current RecursiveIn proofs such as cond_core_rfind still work directly with the inductive constructors and are thus very long. A follow up could add a combinator-style closure library byessentially relativizing all the results and lemmas in Partrec, and proofs could be golfed heavily as they are in Partrec

Note: AI Usage

Aleph prover was allowed to prove an earlier version of cond_core_rfind, which included stating and proving the lemma cond_const but the proofs have since been iterated on manually

Cursor was allowed to run git commands and edit docstrings/headers, and was used in setting up the module structure of the files

[github-actions]

PR summary a2306eca72

Import changes exceeding 2%

%	File
+14.74%	Mathlib.Computability.TuringDegree

Import changes for modified files

Dependency changes

File	Base Count	Head Count	Change
Mathlib.Computability.TuringDegree	604	693	+89 (+14.74%)
Mathlib.Computability.RecursiveIn	602	603	+1 (+0.17%)

Import changes for all files

Files	Import difference
Mathlib.Computability.RecursiveIn	1
Mathlib.Computability.TuringDegree	89

---

Declarations diff

+ Computable.computableIn
+ ComputableIn
+ ComputableIn.recursiveIn'
+ ComputableIn₂
+ ComputableIn₂.recursiveIn₂
+ Nat.Partrec.recursiveIn
+ Primrec.to_computableIn
+ PrimrecIn
+ PrimrecIn'
+ Primrec₂.to_computableIn₂
+ RecursiveIn'
+ RecursiveIn.partrec_of_none
+ RecursiveIn.partrec_of_zero
+ RecursiveIn₂
+ cond
+ cond_const
+ cond_core_rfind
+ const_in
+ even
+ fst_in
+ id_in
+ instSemilatticeSup
+ instance : IsPreorder (ℕ →. ℕ) TuringReducible
+ instance : IsTrans (ℕ →. ℕ) TuringReducible
+ instance : Refl TuringReducible where refl _ := .rfl
+ join
+ join_congr
+ join_le
+ join_mono
+ join_recursiveIn_pair
+ kronecker
+ kronecker_partrec
+ kronecker_rfind
+ kronecker_rfind_none
+ kronecker_rfind_some
+ left_le_join
+ liftPrim
+ liftPrimrec
+ mono
+ none
+ odd
+ of_eq
+ of_eq_tot
+ of_primrec
+ partrec_iff_forall_recursiveIn
+ partrec_of_partrec_oracle
+ right_le_join
+ snd_in
+ some
+ subst
+ succ_in
+ sumInl_in
+ sumInr_in
+ sup
+ sup_def
+ sup_mk
+ unpair_in
- Nat.Partrec.turingReducible
- TuringReducible.partrec_of_zero
- partrec_iff_forall_turingReducible

You can run this locally as follows

## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>

The doc-module for script/declarations_diff.sh contains some details about this script.

---

No changes to technical debt.

You can run this locally as

./scripts/technical-debt-metrics.sh pr_summary

• The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
• The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

[tannerduve]

@eric-wieser note that odifreddi is already in references.bib