Verification of the original Friedberg–Muchnik theorem

This file verifies the finite-injury stage construction of TauCeti.Computability.FriedbergMuchnik.Construction [S, VII.2.1] and proves the Friedberg–Muchnik theorem (friedberg_muchnik) and its Turing-degree corollaries strictly between 0 and 0':

1. restraint_lt_witness_of_notMem and exists_lt_of_mem_injuriesAt: active higher-priority restraints lie strictly below unenumerated lower-priority witnesses, so only k < e can injure requirement e.
2. exists_lt_action_between and the 2 ^ k / 2 ^ e - 1 bounds on attentionStages, enumeratedBy, initializationStages, injurySet, injuryStages, and monitoredInjuryEvents.
3. zero_mem_eval_of_mem_set, zero_notMem_eval_of_notMem_set, and eval_ne_oracle: requirement satisfaction in both stabilization regimes.

References

• R. M. Friedberg, Two recursively enumerable sets of incomparable degrees of unsolvability, Proc. Nat. Acad. Sci. U.S.A. 43 (1957), 236–238.
• A. A. Muchnik, On the unsolvability of the problem of reducibility in the theory of algorithms, Dokl. Akad. Nauk SSSR 108 (1956), 194–197.
• R. I. Soare, Recursively Enumerable Sets and Degrees, Springer, 1987, Theorem VII.2.1.

Stage invariant and injury attribution

theorem TauCeti.FriedbergMuchnik.restraint_lt_witness_of_notMem {i j s b : ℕ} (hij : i < j) (hb : restraint i s = some b) (hw : witness j s ∉ stage (side j) s) : b < witness j s

Restraint–witness invariant. An active higher-priority restraint restraint i s = some b (i < j) lies strictly below any unenumerated lower-priority witness witness j s.

theorem TauCeti.FriedbergMuchnik.exists_lt_of_mem_injuriesAt {e s x : ℕ} (hx : x ∈ Priority.injuriesAt (stage (monitoredSide e)) restraint e s) : ∃ k < e, side k = monitoredSide e ∧ action s = some k ∧ witness k s = x

Injury attribution. Every x ∈ injuriesAt (stage (monitoredSide e)) restraint e s was enumerated by an action of some k < e with side k = monitoredSide e and witness k s = x.

theorem TauCeti.FriedbergMuchnik.exists_lt_of_mem_monitoredInjuryEvents {e s x : ℕ} {b : Bool} (h : (b, s, x) ∈ Priority.monitoredInjuryEvents stage monitoredSide restraint e) : b = monitoredSide e ∧ ∃ k < e, side k = b ∧ action s = some k ∧ witness k s = x

Every labelled injury event in monitoredInjuryEvents comes from an action of some k < e.

Epochs, stabilization, and quantitative bounds

theorem TauCeti.FriedbergMuchnik.witness_eq_of_forall_lt_action_ne {k s₁ s₂ : ℕ} (hs : s₁ ≤ s₂) (hno : ∀ (t : ℕ), s₁ ≤ t → t < s₂ → ∀ i < k, action t ≠ some i) : witness k s₂ = witness k s₁

If no i < k acts in [s₁, s₂), then witness k stays constant from s₁ to s₂.

theorem TauCeti.FriedbergMuchnik.restraint_eq_of_forall_le_action_ne {k s₁ s₂ : ℕ} (hs : s₁ ≤ s₂) (hno : ∀ (t : ℕ), s₁ ≤ t → t < s₂ → ∀ i ≤ k, action t ≠ some i) : restraint k s₂ = restraint k s₁

If no i ≤ k acts in [s₁, s₂), then restraint k stays constant from s₁ to s₂.

theorem TauCeti.FriedbergMuchnik.exists_lt_action_between (k : ℕ) {s₁ s₂ : ℕ} (hlt : s₁ < s₂) (hs₁ : action s₁ = some k) (hs₂ : action s₂ = some k) : ∃ (t : ℕ), s₁ < t ∧ t < s₂ ∧ ∃ i < k, action t = some i

At most one action per epoch. Between any two actions of k, some i < k acts.

theorem TauCeti.FriedbergMuchnik.finite_attentionStages_and_ncard_le (k : ℕ) : (Priority.attentionStages action k).Finite ∧ (Priority.attentionStages action k).ncard ≤ 2 ^ k

Quantitative attention bound 2 ^ k.

theorem TauCeti.FriedbergMuchnik.finite_enumeratedBy_and_ncard_le (k : ℕ) : (enumeratedBy k).Finite ∧ (enumeratedBy k).ncard ≤ 2 ^ k

Requirement k enumerates finitely many numbers, at most 2 ^ k.

theorem TauCeti.FriedbergMuchnik.finite_initializationStages_and_ncard_le (e : ℕ) : (Priority.initializationStages action e).Finite ∧ (Priority.initializationStages action e).ncard ≤ 2 ^ e - 1

Quantitative initialization bound 2 ^ e - 1.

theorem TauCeti.FriedbergMuchnik.finite_injurySet_and_ncard_le (e : ℕ) : (Priority.injurySet (stage (monitoredSide e)) restraint e).Finite ∧ (Priority.injurySet (stage (monitoredSide e)) restraint e).ncard ≤ 2 ^ e - 1

Quantitative injury-set bound 2 ^ e - 1.

theorem TauCeti.FriedbergMuchnik.injurySet_zero_eq_empty : Priority.injurySet (stage (monitoredSide 0)) restraint 0 = ∅

Priority 0 is never injured on its monitored oracle.

theorem TauCeti.FriedbergMuchnik.finite_injuryStages_and_ncard_le (e : ℕ) : (Priority.injuryStages (stage (monitoredSide e)) restraint e).Finite ∧ (Priority.injuryStages (stage (monitoredSide e)) restraint e).ncard ≤ 2 ^ e - 1

Quantitative injury-stages bound 2 ^ e - 1.

theorem TauCeti.FriedbergMuchnik.finite_monitoredInjuryEvents_and_ncard_le (e : ℕ) : (Priority.monitoredInjuryEvents stage monitoredSide restraint e).Finite ∧ (Priority.monitoredInjuryEvents stage monitoredSide restraint e).ncard ≤ 2 ^ e - 1

Quantitative bound on labelled monitoredInjuryEvents.

theorem TauCeti.FriedbergMuchnik.exists_stabilization_stage (k : ℕ) : ∃ (s₀ : ℕ), (∀ s ≥ s₀, ∀ i < k, action s ≠ some i) ∧ (∀ s ≥ s₀, witness k s = witness k s₀) ∧ {s : ℕ | s₀ ≤ s ∧ action s = some k}.Subsingleton

Stabilization and permanent witness. From some stage s₀ onward, no i < k acts, witness k stays at witness k s₀, and k acts at most once.

theorem TauCeti.FriedbergMuchnik.exists_eventually_witness_eq (k : ℕ) : ∃ x ∈ k.pairColumn, ∀ᶠ (s : ℕ) in Filter.atTop, witness k s = x

Every requirement k eventually holds a permanent witness in k.pairColumn.

Satisfaction of requirements and Turing incomparability

theorem TauCeti.FriedbergMuchnik.zero_mem_eval_of_mem_set {k s₀ : ℕ} (hno : ∀ s ≥ s₀, ∀ i < k, action s ≠ some i) (hx : witness k s₀ ∈ set (side k)) : 0 ∈ Oracle.Single.Code.eval (set (monitoredSide k)).oracle (Denumerable.ofNat Oracle.Single.Code (k / 2)) (witness k s₀)

Satisfaction when the permanent witness enters set (side k).

theorem TauCeti.FriedbergMuchnik.zero_notMem_eval_of_notMem_set {k s₀ : ℕ} (hno : ∀ s ≥ s₀, ∀ i < k, action s ≠ some i) (hx : witness k s₀ ∉ set (side k)) : 0 ∉ Oracle.Single.Code.eval (set (monitoredSide k)).oracle (Denumerable.ofNat Oracle.Single.Code (k / 2)) (witness k s₀)

Satisfaction when the permanent witness stays outside set (side k).

theorem TauCeti.FriedbergMuchnik.eval_ne_oracle (k : ℕ) : Oracle.Single.Code.eval (set (monitoredSide k)).oracle (Denumerable.ofNat Oracle.Single.Code (k / 2)) ≠ (set (side k)).oracle

Every requirement R_k is satisfied.

Main theorems and Turing degree corollaries

theorem TauCeti.not_turingReducible_friedbergMuchnikSetA_friedbergMuchnikSetB : ¬TuringReducible friedbergMuchnikSetA.oracle friedbergMuchnikSetB.oracle

friedbergMuchnikSetA is not Turing reducible to friedbergMuchnikSetB.

theorem TauCeti.not_turingReducible_friedbergMuchnikSetB_friedbergMuchnikSetA : ¬TuringReducible friedbergMuchnikSetB.oracle friedbergMuchnikSetA.oracle

friedbergMuchnikSetB is not Turing reducible to friedbergMuchnikSetA.

theorem TauCeti.not_computablePred_mem_friedbergMuchnikSetA : ¬ComputablePred fun (x : ℕ) => x ∈ friedbergMuchnikSetA

friedbergMuchnikSetA is not computable.

theorem TauCeti.not_computablePred_mem_friedbergMuchnikSetB : ¬ComputablePred fun (x : ℕ) => x ∈ friedbergMuchnikSetB

friedbergMuchnikSetB is not computable.

theorem TauCeti.friedberg_muchnik : ∃ (A : Set ℕ) (B : Set ℕ), (REPred fun (x : ℕ) => x ∈ A) ∧ (REPred fun (x : ℕ) => x ∈ B) ∧ ¬TuringReducible A.oracle B.oracle ∧ ¬TuringReducible B.oracle A.oracle

The Friedberg–Muchnik theorem [S, VII.2.1].

theorem TauCeti.degree_friedbergMuchnikSetA_mem_Ioo : toAntisymmetrization TuringReducible friedbergMuchnikSetA.oracle ∈ Set.Ioo (toAntisymmetrization TuringReducible ∅.oracle) (toAntisymmetrization TuringReducible ∅.jump.oracle)

The Turing degree of friedbergMuchnikSetA lies strictly between 0 and 0'.

theorem TauCeti.degree_friedbergMuchnikSetB_mem_Ioo : toAntisymmetrization TuringReducible friedbergMuchnikSetB.oracle ∈ Set.Ioo (toAntisymmetrization TuringReducible ∅.oracle) (toAntisymmetrization TuringReducible ∅.jump.oracle)

The Turing degree of friedbergMuchnikSetB lies strictly between 0 and 0'.

theorem TauCeti.incomparable_degree_friedbergMuchnikSetA_friedbergMuchnikSetB : ¬toAntisymmetrization TuringReducible friedbergMuchnikSetA.oracle ≤ toAntisymmetrization TuringReducible friedbergMuchnikSetB.oracle ∧ ¬toAntisymmetrization TuringReducible friedbergMuchnikSetB.oracle ≤ toAntisymmetrization TuringReducible friedbergMuchnikSetA.oracle

The Turing degrees of friedbergMuchnikSetA and friedbergMuchnikSetB are incomparable.

theorem TauCeti.exists_incomparable_ce_turingDegrees_mem_Ioo : ∃ (A : Set ℕ) (B : Set ℕ), (REPred fun (x : ℕ) => x ∈ A) ∧ (REPred fun (x : ℕ) => x ∈ B) ∧ toAntisymmetrization TuringReducible A.oracle ∈ Set.Ioo (toAntisymmetrization TuringReducible ∅.oracle) (toAntisymmetrization TuringReducible ∅.jump.oracle) ∧ toAntisymmetrization TuringReducible B.oracle ∈ Set.Ioo (toAntisymmetrization TuringReducible ∅.oracle) (toAntisymmetrization TuringReducible ∅.jump.oracle) ∧ ¬toAntisymmetrization TuringReducible A.oracle ≤ toAntisymmetrization TuringReducible B.oracle ∧ ¬toAntisymmetrization TuringReducible B.oracle ≤ toAntisymmetrization TuringReducible A.oracle

Degree form of the Friedberg–Muchnik theorem.