Documentation

MIPRE.Tailored.Halting.Induction

The tailored halting verifier: the values at level C #

Paper II, II:2021–2066 (the main theorem from compression), along the route of MIPRE/Foundations/Halting/Paper/Induction.lean, which this file parallels: for a machine M and a parameter λ such that V^{M,λ} is λ-bounded,

with C = max C₀ 2. The argument runs along the levels C, 2 ^ C, 2 ^ (2 ^ C), … of the recursion (lv). The two classes are A n, a perfect ZPC strategy at level n, and B n, value at most 1/2 there. TailoredGapCompression.completeness and soundness carry A (2 ^ n) → A n and B (2 ^ n) → B n at every level where neither of the processor's first two branches fires (lem:dhalt-values); branch 1 puts a level in A outright and branch 2 in B; and the search halts exactly when the start level has value above 1/2, which rules the search out below the level where M halts, and the start level out of B's complement when M does not.

Unlike the existing halting layer, there is no answer bound to carry along: the answers of a tailored game have the lengths its answer-length calculator gives them.

The search program is a parameter, with its specification SearchSpec: on the description of a λ-bounded tailored verifier (S^λ, L^λ, P) it halts exactly when the value at level C exceeds 1/2. A program meeting it comes from tabulating a tailored verifier at a fixed level, the next part of the plan.

The levels #

source
def MIPRE.Tailored.Halting.C {ℓ : ℕ} (TG : TailoredGapCompression ℓ) :
ℕ

The level the reduction outputs: max C₀ 2, so that the time clauses of IsBounded apply there.

Equations
Instances For
    source
    theorem MIPRE.Tailored.Halting.two_le_C {ℓ : ℕ} (TG : TailoredGapCompression ℓ) :
    2 ≤ C TG
    source
    theorem MIPRE.Tailored.Halting.C₀_le_C {ℓ : ℕ} (TG : TailoredGapCompression ℓ) :
    TG.C₀ ≤ C TG
    source
    def MIPRE.Tailored.Halting.lv {ℓ : ℕ} (TG : TailoredGapCompression ℓ) :
    ℕ → ℕ

    The levels of the recursion started at C: C, 2 ^ C, 2 ^ (2 ^ C), ….

    Equations
    Instances For
      source
      @[simp]
      theorem MIPRE.Tailored.Halting.lv_zero {ℓ : ℕ} (TG : TailoredGapCompression ℓ) :
      lv TG 0 = C TG
      source
      @[simp]
      theorem MIPRE.Tailored.Halting.lv_succ {ℓ : ℕ} (TG : TailoredGapCompression ℓ) (j : ℕ) :
      lv TG (j + 1) = 2 ^ lv TG j
      source
      theorem MIPRE.Tailored.Halting.two_pow_le_lv {ℓ : ℕ} (TG : TailoredGapCompression ℓ) (j : ℕ) :
      2 ^ j ≤ lv TG j
      source
      theorem MIPRE.Tailored.Halting.C_le_lv {ℓ : ℕ} (TG : TailoredGapCompression ℓ) (j : ℕ) :
      C TG ≤ lv TG j
      source
      theorem MIPRE.Tailored.Halting.lv_mono {ℓ : ℕ} (TG : TailoredGapCompression ℓ) {j k : ℕ} (h : j ≤ k) :
      lv TG j ≤ lv TG k
      source
      theorem MIPRE.Tailored.Halting.exists_le_size_lv {ℓ : ℕ} (TG : TailoredGapCompression ℓ) (k : ℕ) :
      ∃ (j : ℕ), k ≤ (lv TG j).size

      The branches along the levels #

      source
      theorem MIPRE.Tailored.Halting.branch_mono {p : Cost.Prog} {n n' : ℕ} (h : n.size ≤ n'.size) (hp : (Cost.evalWithin p Cost.Data.nil n.size).isSome = true) :
      (Cost.evalWithin p Cost.Data.nil n'.size).isSome = true
      source
      theorem MIPRE.Tailored.Halting.branch1_of_halts {M : Cost.Prog} (hM : Cost.Halts M Cost.Data.nil) :
      ∃ (k : ℕ), ∀ (n : ℕ), k ≤ n.size → branch1 M n
      source
      theorem MIPRE.Tailored.Halting.not_branch1_of_not_halts {M : Cost.Prog} (hM : ¬Cost.Halts M Cost.Data.nil) (n : ℕ) :
      ¬branch1 M n
      source
      def MIPRE.Tailored.Halting.vof {ℓ : ℕ} (TG : TailoredGapCompression ℓ) (lam : ℕ) (P : Decider) :
      TailoredVerifier ℓ

      The tailored verifier (S^λ, L^λ, P) that a parameter and a processor describe.

      Equations
      Instances For
        source
        theorem MIPRE.Tailored.Halting.Vhalt_eq_vof {ℓ : ℕ} (TG : TailoredGapCompression ℓ) (U : Cost.UniversalMachine) (UT : Cost.ClockedUniversalMachine) (S' M : Cost.Prog) (lam : ℕ) :
        Vhalt TG U UT S' M lam = vof TG lam (lp TG U UT S' M lam)
        source
        def MIPRE.Tailored.Halting.SearchSpec {ℓ : ℕ} (TG : TailoredGapCompression ℓ) (S' : Cost.Prog) (m : ℕ) :
        Prop

        The specification of the search program at the level m: on the description descOf λ P of a λ-bounded tailored verifier (S^λ, L^λ, P), it halts exactly when the value at level m exceeds 1/2.

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For

          The two classes #

          source
          def MIPRE.Tailored.Halting.A {ℓ : ℕ} (TG : TailoredGapCompression ℓ) (U : Cost.UniversalMachine) (UT : Cost.ClockedUniversalMachine) (S' M : Cost.Prog) (lam n : ℕ) :
          Prop

          The class A at level n: a perfect ZPC strategy.

          Equations
          Instances For
            source
            def MIPRE.Tailored.Halting.B {ℓ : ℕ} (TG : TailoredGapCompression ℓ) (U : Cost.UniversalMachine) (UT : Cost.ClockedUniversalMachine) (S' M : Cost.Prog) (lam n : ℕ) :
            Prop

            The class B at level n: value at most 1/2.

            Equations
            Instances For
              source
              theorem MIPRE.Tailored.Halting.A_of_branch1 {ℓ : ℕ} (TG : TailoredGapCompression ℓ) (U : Cost.UniversalMachine) (UT : Cost.ClockedUniversalMachine) {S' M : Cost.Prog} {lam n : ℕ} (h1 : branch1 M n) :
              A TG U UT S' M lam n
              source
              theorem MIPRE.Tailored.Halting.B_of_branch2 {ℓ : ℕ} (TG : TailoredGapCompression ℓ) (U : Cost.UniversalMachine) (UT : Cost.ClockedUniversalMachine) {S' M : Cost.Prog} {lam n : ℕ} (h1 : ¬branch1 M n) (h2 : branch2 TG U UT S' M lam n) :
              B TG U UT S' M lam n
              source
              theorem MIPRE.Tailored.Halting.A_step {ℓ : ℕ} (TG : TailoredGapCompression ℓ) (U : Cost.UniversalMachine) (UT : Cost.ClockedUniversalMachine) {S' M : Cost.Prog} {lam : ℕ} (hb : (Vhalt TG U UT S' M lam).IsBounded lam) {n : ℕ} (hn : C TG ≤ n) (h1 : ¬branch1 M n) (h2 : ¬branch2 TG U UT S' M lam n) (hA : A TG U UT S' M lam (2 ^ n)) :
              A TG U UT S' M lam n

              Completeness carried down a level, where neither branch fires.

              source
              theorem MIPRE.Tailored.Halting.B_step {ℓ : ℕ} (TG : TailoredGapCompression ℓ) (U : Cost.UniversalMachine) (UT : Cost.ClockedUniversalMachine) {S' M : Cost.Prog} {lam : ℕ} (hb : (Vhalt TG U UT S' M lam).IsBounded lam) {n : ℕ} (hn : C TG ≤ n) (h1 : ¬branch1 M n) (h2 : ¬branch2 TG U UT S' M lam n) (hB : B TG U UT S' M lam (2 ^ n)) :
              B TG U UT S' M lam n

              Soundness carried down a level, where neither branch fires.

              source
              theorem MIPRE.Tailored.Halting.B_below {ℓ : ℕ} (TG : TailoredGapCompression ℓ) (U : Cost.UniversalMachine) (UT : Cost.ClockedUniversalMachine) {S' M : Cost.Prog} {lam : ℕ} (hb : (Vhalt TG U UT S' M lam).IsBounded lam) (j₀ : ℕ) (hnot : ¬branch1 M (lv TG j₀)) (hfire : branch2 TG U UT S' M lam (lv TG j₀)) (i j : ℕ) :
              j + i = j₀ → B TG U UT S' M lam (lv TG j)

              Below a level where the search fires while M has not halted, every level of the recursion is in B.

              source
              theorem MIPRE.Tailored.Halting.halts_search_iff {ℓ : ℕ} (TG : TailoredGapCompression ℓ) (U : Cost.UniversalMachine) (UT : Cost.ClockedUniversalMachine) {S' M : Cost.Prog} {lam : ℕ} (hb : (Vhalt TG U UT S' M lam).IsBounded lam) (hS' : Cost.Prog.WellScoped 1 S') (hsem : SearchSpec TG S' (C TG)) :
              Cost.Halts (Halting.searchP S' lam (lpProg TG U UT S' M lam)) Cost.Data.nil ↔ 1 / 2 < (Vhalt TG U UT S' M lam).valStar (C TG)

              The search halts exactly when the start level has value above 1/2.

              source
              theorem MIPRE.Tailored.Halting.branch2_of_lt {ℓ : ℕ} (TG : TailoredGapCompression ℓ) (U : Cost.UniversalMachine) (UT : Cost.ClockedUniversalMachine) {S' M : Cost.Prog} {lam : ℕ} (hb : (Vhalt TG U UT S' M lam).IsBounded lam) (hS' : Cost.Prog.WellScoped 1 S') (hsem : SearchSpec TG S' (C TG)) (h : 1 / 2 < (Vhalt TG U UT S' M lam).valStar (C TG)) :
              ∃ (k : ℕ), ∀ (n : ℕ), k ≤ n.size → branch2 TG U UT S' M lam n
              source
              theorem MIPRE.Tailored.Halting.lt_of_branch2 {ℓ : ℕ} (TG : TailoredGapCompression ℓ) (U : Cost.UniversalMachine) (UT : Cost.ClockedUniversalMachine) {S' M : Cost.Prog} {lam : ℕ} (hb : (Vhalt TG U UT S' M lam).IsBounded lam) (hS' : Cost.Prog.WellScoped 1 S') (hsem : SearchSpec TG S' (C TG)) {n : ℕ} (h2 : branch2 TG U UT S' M lam n) :
              1 / 2 < (Vhalt TG U UT S' M lam).valStar (C TG)

              The two cases #

              source
              theorem MIPRE.Tailored.Halting.hasPerfectZPC_of_halts {ℓ : ℕ} (TG : TailoredGapCompression ℓ) (U : Cost.UniversalMachine) (UT : Cost.ClockedUniversalMachine) {S' M : Cost.Prog} {lam : ℕ} (hb : (Vhalt TG U UT S' M lam).IsBounded lam) (hS' : Cost.Prog.WellScoped 1 S') (hsem : SearchSpec TG S' (C TG)) (hM : Cost.Halts M Cost.Data.nil) :
              (Vhalt TG U UT S' M lam).HasPerfectZPC (C TG)

              The halting case: V^{M,λ} has a perfect ZPC strategy at level C.

              source
              theorem MIPRE.Tailored.Halting.valStar_le_of_not_halts {ℓ : ℕ} (TG : TailoredGapCompression ℓ) (U : Cost.UniversalMachine) (UT : Cost.ClockedUniversalMachine) {S' M : Cost.Prog} {lam : ℕ} (hb : (Vhalt TG U UT S' M lam).IsBounded lam) (hS' : Cost.Prog.WellScoped 1 S') (hsem : SearchSpec TG S' (C TG)) (hM : ¬Cost.Halts M Cost.Data.nil) :
              (Vhalt TG U UT S' M lam).valStar (C TG) ≤ 1 / 2

              The non-halting case: val*(V^{M,λ}_C) ≤ 1/2.