# Rigidity of the Turing degrees

The following describes the scope of the Lean formalization related to the following accompanying paper(s):

- [Rigidity of the Turing degrees](../../preprints/Rigidity-of-the-Turing-degrees-September-24-2026/paper.pdf)

## Scope

The rigidity problem asks whether the ordering of Turing degrees by relative computability has any nontrivial automorphism. The formalized result gives a negative answer: every order automorphism of the full Turing degrees of subsets of $\mathbb N$ fixes every degree, with no definability or genericity assumption. The additional representation corollaries are not included.

## Comparator links

| Result | Comparator statement |
| --- | --- |
| Rigidity of the Turing degrees | [DegreeRigidity.lean](../ComparatorChallenges/DegreeRigidity.lean) |