The halting verifier along the paper's route: the values at level C

Blueprint thm:halting in the paper's form, at a fixed level, from the decider of Paper/Decider.lean and gap-preserving compression: for a machine M and a parameter λ such that 𝒱^halt_{M,λ} is λ-bounded (the accounting of Paper/Cost.lean supplies one),

• if M halts on the empty input, 𝒱^halt has a value-1 PCC strategy at level C;
• if it does not, val*(𝒱^halt_C) ≤ 1/2;

with C = max C₀ 2 and answers of length at most G.bound (C + λ).

The argument is the criterion's (Cost.compressibility_criterion_levels) at the fixed level C, along the levels C, 2 ^ C, 2 ^ (2 ^ C), … of the recursion (lv): the two classes are A n, a value-1 PCC strategy at level n with answers of length at most n ^ λ, and B n, value at most 1/2 there; GapCompression.completeness and soundness carry A (2 ^ n) → A n and B (2 ^ n) → B n at every level where neither of the decider's first two branches fires (lem:dhalt-values, the acceptance agreement with the compressed verifier); 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 (exists_semL, tabL_value), which is what rules the search out below the level where M halts, and rules the start level out of B's complement when M does not.

def MIPRE.Halting.C (G : GapCompression) : ℕ

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

Equations

• MIPRE.Halting.C G = max G.C₀ 2

theorem MIPRE.Halting.two_le_C (G : GapCompression) : 2 ≤ C G

theorem MIPRE.Halting.C₀_le_C (G : GapCompression) : G.C₀ ≤ C G

def MIPRE.Halting.lv (G : GapCompression) : ℕ → ℕ

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

Equations

• MIPRE.Halting.lv G 0 = MIPRE.Halting.C G
• MIPRE.Halting.lv G j.succ = 2 ^ MIPRE.Halting.lv G j

@[simp]

theorem MIPRE.Halting.lv_zero (G : GapCompression) : lv G 0 = C G

@[simp]

theorem MIPRE.Halting.lv_succ (G : GapCompression) (j : ℕ) : lv G (j + 1) = 2 ^ lv G j

theorem MIPRE.Halting.two_pow_le_lv (G : GapCompression) (j : ℕ) : 2 ^ j ≤ lv G j

theorem MIPRE.Halting.C_le_lv (G : GapCompression) (j : ℕ) : C G ≤ lv G j

theorem MIPRE.Halting.lv_mono (G : GapCompression) {j k : ℕ} (h : j ≤ k) : lv G j ≤ lv G k

theorem MIPRE.Halting.exists_le_size_lv (G : GapCompression) (k : ℕ) : ∃ (j : ℕ), k ≤ (lv G j).size

@[reducible, inline]

noncomputable abbrev MIPRE.Halting.W (G : GapCompression) (U : Cost.UniversalMachine) (UT : Cost.ClockedUniversalMachine) (S' M : Cost.Prog) (lam : ℕ) : Verifier 7

The compressed verifier of 𝒱^halt, the same at every level.

Equations

• MIPRE.Halting.W G U UT S' M lam = G.output ((MIPRE.Halting.Vhalt G U UT S' M lam).sampler.prog, (MIPRE.Halting.Vhalt G U UT S' M lam).decider.prog) lam

def MIPRE.Halting.branch1 (M : Cost.Prog) (n : ℕ) : Prop

The first branch fires: M halts within Nat.size n.

Equations

• MIPRE.Halting.branch1 M n = ((MIPRE.Cost.evalWithin M MIPRE.Cost.Data.nil n.size).isSome = true)

def MIPRE.Halting.branch2 (G : GapCompression) (U : Cost.UniversalMachine) (UT : Cost.ClockedUniversalMachine) (S' M : Cost.Prog) (lam n : ℕ) : Prop

The second branch fires: the search halts within Nat.size n.

Equations

• MIPRE.Halting.branch2 G U UT S' M lam n = ((MIPRE.Cost.evalWithin (MIPRE.Halting.searchP S' lam (MIPRE.Halting.dec G U UT S' M lam)) MIPRE.Cost.Data.nil n.size).isSome = true)

theorem MIPRE.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

theorem MIPRE.Halting.branch1_of_halts {M : Cost.Prog} (hM : Cost.Halts M Cost.Data.nil) : ∃ (k : ℕ), ∀ (n : ℕ), k ≤ n.size → branch1 M n

theorem MIPRE.Halting.not_branch1_of_not_halts {M : Cost.Prog} (hM : ¬Cost.Halts M Cost.Data.nil) (n : ℕ) : ¬branch1 M n

The acceptance of 𝒱^halt at a level, by branch

theorem MIPRE.Halting.accepts_diag_of_branch1 (G : GapCompression) (U : Cost.UniversalMachine) (UT : Cost.ClockedUniversalMachine) {S' : Cost.Prog} (M : Cost.Prog) (lam : ℕ) {n : ℕ} (h1 : branch1 M n) (x y : (Vhalt G U UT S' M lam).Questions n) : (Vhalt G U UT S' M lam).decider.Accepts n (CL.toBits x) (CL.toBits y) [] []

theorem MIPRE.Halting.rejects_all_of_branch2 (G : GapCompression) (U : Cost.UniversalMachine) (UT : Cost.ClockedUniversalMachine) {S' : Cost.Prog} (M : Cost.Prog) (lam : ℕ) {n : ℕ} (h1 : ¬branch1 M n) (h2 : branch2 G U UT S' M lam n) (x y a b : Cost.BitStr) : ¬(Vhalt G U UT S' M lam).decider.Accepts n x y a b

theorem MIPRE.Halting.accepts_iff_W (G : GapCompression) (U : Cost.UniversalMachine) (UT : Cost.ClockedUniversalMachine) {S' : Cost.Prog} (M : Cost.Prog) (lam : ℕ) {n : ℕ} (h1 : ¬branch1 M n) (h2 : ¬branch2 G U UT S' M lam n) (x y a b : Cost.BitStr) : (Vhalt G U UT S' M lam).decider.Accepts n x y a b ↔ (W G U UT S' M lam).decider.Accepts n x y a b

theorem MIPRE.Halting.W_sampler (G : GapCompression) (U : Cost.UniversalMachine) (UT : Cost.ClockedUniversalMachine) {S' : Cost.Prog} (M : Cost.Prog) (lam : ℕ) : (W G U UT S' M lam).sampler = (Vhalt G U UT S' M lam).sampler

theorem MIPRE.Halting.rejectsLong_of_not_branch1 (G : GapCompression) (U : Cost.UniversalMachine) (UT : Cost.ClockedUniversalMachine) {S' : Cost.Prog} (M : Cost.Prog) (lam : ℕ) {n : ℕ} (h1 : ¬branch1 M n) : (Vhalt G U UT S' M lam).RejectsLong n (Polynomial.eval (n + lam) G.bound)

Below the first branch, 𝒱^halt rejects every answer longer than the compressed bound.

The two classes and the compression steps

def MIPRE.Halting.A (G : GapCompression) (U : Cost.UniversalMachine) (UT : Cost.ClockedUniversalMachine) (S' M : Cost.Prog) (lam n : ℕ) : Prop

The class A at level n: a value-1 PCC strategy with answers of length at most n ^ λ.

Equations

• MIPRE.Halting.A G U UT S' M lam n = (MIPRE.Halting.Vhalt G U UT S' M lam).HasPerfectPCC n (n ^ lam)

def MIPRE.Halting.B (G : GapCompression) (U : Cost.UniversalMachine) (UT : Cost.ClockedUniversalMachine) (S' M : Cost.Prog) (lam n : ℕ) : Prop

The class B at level n: value at most 1/2 with answers of length at most n ^ λ.

Equations

• MIPRE.Halting.B G U UT S' M lam n = ((MIPRE.Halting.Vhalt G U UT S' M lam).valStar n (n ^ lam) ≤ 1 / 2)

theorem MIPRE.Halting.A_of_branch1 (G : GapCompression) (U : Cost.UniversalMachine) (UT : Cost.ClockedUniversalMachine) {S' : Cost.Prog} (M : Cost.Prog) (lam : ℕ) {n : ℕ} (h1 : branch1 M n) : A G U UT S' M lam n

theorem MIPRE.Halting.B_of_branch2 (G : GapCompression) (U : Cost.UniversalMachine) (UT : Cost.ClockedUniversalMachine) {S' : Cost.Prog} (M : Cost.Prog) (lam : ℕ) {n : ℕ} (h1 : ¬branch1 M n) (h2 : branch2 G U UT S' M lam n) : B G U UT S' M lam n

theorem MIPRE.Halting.A_step (G : GapCompression) (U : Cost.UniversalMachine) (UT : Cost.ClockedUniversalMachine) {S' : Cost.Prog} (M : Cost.Prog) (lam : ℕ) (hb : (Vhalt G U UT S' M lam).IsBounded lam) {n : ℕ} (hn : C G ≤ n) (h1 : ¬branch1 M n) (h2 : ¬branch2 G U UT S' M lam n) (hA : A G U UT S' M lam (2 ^ n)) : (Vhalt G U UT S' M lam).HasPerfectPCC n (Polynomial.eval (n + lam) G.bound)

Completeness carried down a level, where neither branch fires.

theorem MIPRE.Halting.A_step' (G : GapCompression) (U : Cost.UniversalMachine) (UT : Cost.ClockedUniversalMachine) {S' : Cost.Prog} (M : Cost.Prog) (lam : ℕ) (hb : (Vhalt G U UT S' M lam).IsBounded lam) (hpoly : ∀ (n : ℕ), 2 ≤ n → Polynomial.eval (n + lam) G.bound ≤ n ^ lam) {n : ℕ} (hn : C G ≤ n) (h1 : ¬branch1 M n) (h2 : ¬branch2 G U UT S' M lam n) (hA : A G U UT S' M lam (2 ^ n)) : A G U UT S' M lam n

theorem MIPRE.Halting.B_step (G : GapCompression) (U : Cost.UniversalMachine) (UT : Cost.ClockedUniversalMachine) {S' : Cost.Prog} (M : Cost.Prog) (lam : ℕ) (hb : (Vhalt G U UT S' M lam).IsBounded lam) (hpoly : ∀ (n : ℕ), 2 ≤ n → Polynomial.eval (n + lam) G.bound ≤ n ^ lam) {n : ℕ} (hn : C G ≤ n) (h1 : ¬branch1 M n) (h2 : ¬branch2 G U UT S' M lam n) (hB : B G U UT S' M lam (2 ^ n)) : B G U UT S' M lam n

Soundness carried down a level, where neither branch fires.

The search and the start level

theorem MIPRE.Halting.halts_search_iff (G : GapCompression) (U : Cost.UniversalMachine) (UT : Cost.ClockedUniversalMachine) {S' : Cost.Prog} (hS' : Cost.Prog.WellScoped 1 S') (hsem : ∀ (x : Cost.BitStr), Cost.Halts S' (Cost.encode x) ↔ 1 / 2 < quantumValue (tabL G U x (C G)).game) (M : Cost.Prog) (lam : ℕ) (hb : (Vhalt G U UT S' M lam).IsBounded lam) : Cost.Halts (searchP S' lam (dec G U UT S' M lam)) Cost.Data.nil ↔ 1 / 2 < (Vhalt G U UT S' M lam).valStar (C G) (Polynomial.eval (C G + lam) G.bound)

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

theorem MIPRE.Halting.branch2_of_lt (G : GapCompression) (U : Cost.UniversalMachine) (UT : Cost.ClockedUniversalMachine) {S' : Cost.Prog} (hS' : Cost.Prog.WellScoped 1 S') (hsem : ∀ (x : Cost.BitStr), Cost.Halts S' (Cost.encode x) ↔ 1 / 2 < quantumValue (tabL G U x (C G)).game) (M : Cost.Prog) (lam : ℕ) (hb : (Vhalt G U UT S' M lam).IsBounded lam) (h : 1 / 2 < (Vhalt G U UT S' M lam).valStar (C G) (Polynomial.eval (C G + lam) G.bound)) : ∃ (k : ℕ), ∀ (n : ℕ), k ≤ n.size → branch2 G U UT S' M lam n

theorem MIPRE.Halting.lt_of_branch2 (G : GapCompression) (U : Cost.UniversalMachine) (UT : Cost.ClockedUniversalMachine) {S' : Cost.Prog} (hS' : Cost.Prog.WellScoped 1 S') (hsem : ∀ (x : Cost.BitStr), Cost.Halts S' (Cost.encode x) ↔ 1 / 2 < quantumValue (tabL G U x (C G)).game) (M : Cost.Prog) (lam : ℕ) (hb : (Vhalt G U UT S' M lam).IsBounded lam) {n : ℕ} (h2 : branch2 G U UT S' M lam n) : 1 / 2 < (Vhalt G U UT S' M lam).valStar (C G) (Polynomial.eval (C G + lam) G.bound)

theorem MIPRE.Halting.le_of_B_start (G : GapCompression) (U : Cost.UniversalMachine) (UT : Cost.ClockedUniversalMachine) {S' : Cost.Prog} (M : Cost.Prog) (lam : ℕ) (hpoly : ∀ (n : ℕ), 2 ≤ n → Polynomial.eval (n + lam) G.bound ≤ n ^ lam) (h1 : ¬branch1 M (C G)) (hB : B G U UT S' M lam (C G)) : (Vhalt G U UT S' M lam).valStar (C G) (Polynomial.eval (C G + lam) G.bound) ≤ 1 / 2

The start level is in B only if its value is at most 1/2 — with the answer bound of the statement, once the first branch does not fire there.

The two cases

theorem MIPRE.Halting.B_below (G : GapCompression) (U : Cost.UniversalMachine) (UT : Cost.ClockedUniversalMachine) {S' : Cost.Prog} (M : Cost.Prog) (lam : ℕ) (hb : (Vhalt G U UT S' M lam).IsBounded lam) (hpoly : ∀ (n : ℕ), 2 ≤ n → Polynomial.eval (n + lam) G.bound ≤ n ^ lam) (j₀ : ℕ) (hnot : ¬branch1 M (lv G j₀)) (hfire : branch2 G U UT S' M lam (lv G j₀)) (i j : ℕ) : j + i = j₀ → B G U UT S' M lam (lv G j)

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

theorem MIPRE.Halting.hasPerfectPCC_of_halts (G : GapCompression) (U : Cost.UniversalMachine) (UT : Cost.ClockedUniversalMachine) {S' : Cost.Prog} (hS' : Cost.Prog.WellScoped 1 S') (hsem : ∀ (x : Cost.BitStr), Cost.Halts S' (Cost.encode x) ↔ 1 / 2 < quantumValue (tabL G U x (C G)).game) (M : Cost.Prog) (lam : ℕ) (hb : (Vhalt G U UT S' M lam).IsBounded lam) (hpoly : ∀ (n : ℕ), 2 ≤ n → Polynomial.eval (n + lam) G.bound ≤ n ^ lam) (hM : Cost.Halts M Cost.Data.nil) : (Vhalt G U UT S' M lam).HasPerfectPCC (C G) (Polynomial.eval (C G + lam) G.bound)

The halting case: 𝒱^halt has a value-1 PCC strategy at level C.

theorem MIPRE.Halting.valStar_le_of_not_halts (G : GapCompression) (U : Cost.UniversalMachine) (UT : Cost.ClockedUniversalMachine) {S' : Cost.Prog} (hS' : Cost.Prog.WellScoped 1 S') (hsem : ∀ (x : Cost.BitStr), Cost.Halts S' (Cost.encode x) ↔ 1 / 2 < quantumValue (tabL G U x (C G)).game) (M : Cost.Prog) (lam : ℕ) (hb : (Vhalt G U UT S' M lam).IsBounded lam) (hpoly : ∀ (n : ℕ), 2 ≤ n → Polynomial.eval (n + lam) G.bound ≤ n ^ lam) (hM : ¬Cost.Halts M Cost.Data.nil) : (Vhalt G U UT S' M lam).valStar (C G) (Polynomial.eval (C G + lam) G.bound) ≤ 1 / 2

The non-halting case: val*(𝒱^halt_C) ≤ 1/2.