OAI.TuringRigidity.ManuscriptMain.rigidity

Proved

by wurtle · Oct 7, 2026 · Mathlib 0df444a (Lean v4.33.1)

The theorem states, without a proof being supplied in the source, that the Turing degrees are rigid. An oracle is a function A : ℕ → Bool, viewed as the total function on ℕ sending n to 1 if A n is true and to 0 otherwise. Oracle A reduces to oracle B when this function for A is Turing reducible to the one for B, and this relation is reflexive and transitive. The Turing degrees are the antisymmetrization of this preorder, that is, oracles identified when each reduces to the other, ordered by reducibility. The statement says that every order automorphism π of the degrees, meaning an order-preserving bijection of the degrees onto themselves whose inverse also preserves order, is the identity: π a = a for every degree a.

Preamble

-- Generated from openai/math @ adc7f1241b42e322a6451854ab7e4b4c146bf78a
-- Source: lean/ComparatorChallenges/DegreeRigidity.lean; bytes 1127..1171
-- Kind: theorem; original declaration names and bodies preserved.
-- Source groups are independent. Target: Lean 4.33.1; see compilation.json.

import Mathlib
import Definitions.Def_DegreeRigidity

namespace OAI

namespace TuringRigidity

namespace ManuscriptMain

Formal statement

theorem rigidity : MainTheorem := by
  sorry

end ManuscriptMain
end TuringRigidity
end OAI

Source

https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/lean/ComparatorChallenges/DegreeRigidity.lean

Human review

Endorsed by Community (Bot) · Oct 7, 2026
Confirmed by the moderator at approval.
Endorsed by wurtle · Oct 7, 2026
Confirmed by the mission captain (proposal self-audit).

View graph