Computability

Results named in Tau Ceti's TauCeti.Computability modules and in no roadmap's section, as Tau Ceti has them at commit ace60277.

TheoremDegree form of the Friedberg–Muchnik theorem#

TauCeti.exists_incomparable_ce_turingDegrees_mem_Ioo :
  ∃ A B,
    (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

Lean

Formalized in Tau Ceti as TauCeti.exists_incomparable_ce_turingDegrees_mem_Ioo.

Sources

• Tau Ceti documentation: TauCeti.exists_incomparable_ce_turingDegrees_mem_Ioo
• Source of TauCeti.exists_incomparable_ce_turingDegrees_mem_Ioo in TauCeti/Computability/FriedbergMuchnik/Basic.lean

LeanTauCeti.exists_incomparable_ce_turingDegrees_mem_Ioo

TheoremEilenberg's theorem#

for 2 ≤ k, a sequence is k-automatic if and only if its k-kernel is finite.

TauCeti.isAutomatic_iff_finite_kernel.{u} {k : ℕ} {Δ : Type u} {a : ℕ → Δ} [NeZero k] (hk : 2 ≤ k) :
  TauCeti.IsAutomatic k a ↔ (TauCeti.kernel k a).Finite

Lean

Formalized in Tau Ceti as TauCeti.isAutomatic_iff_finite_kernel.

Sources

• Tau Ceti documentation: TauCeti.isAutomatic_iff_finite_kernel
• Source of TauCeti.isAutomatic_iff_finite_kernel in TauCeti/Computability/AutomaticSequence/Kernel.lean

LeanTauCeti.isAutomatic_iff_finite_kernel

TheoremThe Friedberg–Muchnik theorem [S, VII.2.1]#

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

Lean

Formalized in Tau Ceti as TauCeti.friedberg_muchnik.

Sources

• Tau Ceti documentation: TauCeti.friedberg_muchnik
• Source of TauCeti.friedberg_muchnik in TauCeti/Computability/FriedbergMuchnik/Basic.lean

LeanTauCeti.friedberg_muchnik

TheoremSoare's Lemma 1#

Let A and C be the limits of monotone stages whose binary codes are computable, and let requirement e hold, at every stage s, a restraint at least the agreement restraint of the program c against A s with target C s and fuel s. If only finitely many numbers injure e, and c relative to the limit of A computes the characteristic function of the limit of C, then the limit of C is computable.

TauCeti.Oracle.Single.Code.computablePred_mem_stageLimit_of_eval_eq {A C : ℕ → Finset ℕ}
  {r : ℕ → ℕ → Option ℕ} {e : ℕ} {c : TauCeti.Oracle.Single.Code} (hA : Monotone A)
  (hC : Monotone C) (hAc : Computable fun s => Finset.equivBitIndices.symm (A s))
  (hCc : Computable fun s => Finset.equivBitIndices.symm (C s))
  (hr :
    ∀ (s : ℕ),
      ∃ b,
        r e s = some b ∧
          TauCeti.Oracle.Single.Code.agreementRestraint
              (TauCeti.Oracle.Single.Code.setAnswers ↑(A s)) s c ((↑(C s)).indicator 1) ≤
            b)
  (hI : (TauCeti.Priority.injurySet A r e).Finite)
  (heval :
    TauCeti.Oracle.Single.Code.eval (TauCeti.Enumeration.stageLimit A).oracle c =
      (TauCeti.Enumeration.stageLimit C).oracle) :
  ComputablePred fun x => x ∈ TauCeti.Enumeration.stageLimit C

Lean

Formalized in Tau Ceti as TauCeti.Oracle.Single.Code.computablePred_mem_stageLimit_of_eval_eq.

Other forms

Soare's Lemma 1, correctness of late agreement. Formalized in Tau Ceti as TauCeti.Oracle.Single.Code.mem_stageLimit_iff_of_lt_agreementLength.

TauCeti.Oracle.Single.Code.mem_stageLimit_iff_of_lt_agreementLength {A C : ℕ → Finset ℕ}
  {r : ℕ → ℕ → Option ℕ} {e s x : ℕ} {c : TauCeti.Oracle.Single.Code} {s₀ : ℕ} (hA : Monotone A)
  (hC : Monotone C)
  (hr :
    ∀ (s : ℕ),
      s₀ ≤ s →
        ∃ b,
          r e s = some b ∧
            TauCeti.Oracle.Single.Code.agreementRestraint
                (TauCeti.Oracle.Single.Code.setAnswers ↑(A s)) s c ((↑(C s)).indicator 1) ≤
              b)
  (hI : ∀ (s : ℕ), s₀ ≤ s → TauCeti.Priority.injuriesAt A r e s = ∅)
  (heval :
    ∀ y ≤ x,
      TauCeti.Oracle.Single.Code.eval (TauCeti.Enumeration.stageLimit A).oracle c y =
        (TauCeti.Enumeration.stageLimit C).oracle y)
  (hs : s₀ ≤ s)
  (hx :
    x <
      TauCeti.Oracle.Single.Code.agreementLength (TauCeti.Oracle.Single.Code.setAnswers ↑(A s)) s c
        ((↑(C s)).indicator 1)) :
  x ∈ TauCeti.Enumeration.stageLimit C ↔ x ∈ C s

Sources

• Tau Ceti documentation: TauCeti.Oracle.Single.Code.computablePred_mem_stageLimit_of_eval_eq
• Source of TauCeti.Oracle.Single.Code.computablePred_mem_stageLimit_of_eval_eq in TauCeti/Computability/Priority/Agreement/Basic.lean

LeanTauCeti.Oracle.Single.Code.computablePred_mem_stageLimit_of_eval_eq · TauCeti.Oracle.Single.Code.mem_stageLimit_iff_of_lt_agreementLength

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.