The halting verifier along the paper's route: thm:halting at a fixed level

Blueprint thm:halting in the paper's form (recursive.tex), for the polynomial-time halting reduction of planning/polytime-halting.md: for every machine M and every λ ≥ Λ₀ + 4|M|, the verifier 𝒱^halt M λ of Paper/Decider.lean, at the fixed level C = max C₀ 2, has a value-1 PCC strategy if M halts on the empty input and value at most 1/2 otherwise — with the answer alphabet cut at the compressor's bound poly(C, λ), a polynomial in λ.

This is the criterion route's thm:halting (Halting/Reduction.lean, Criterion.lean) with the level fixed and the parameter explicit, which is what makes the reduction polynomial-time: the game is 𝒱^halt M λ at index C, its sampler is the compressed sampler at λ = Λ₀ + 4|M| (polynomial-time in |M| through samplerProg), and its decider runs within the polynomial bound of Paper/Cost.lean. The class verifier of the paper's MIP* (PR 3 of the plan) is this game read off a uniform program.

The search program S' of the decider's second branch is semL, the semidecider of "val* at level C of the verifier this string describes exceeds 1/2" (exists_semL), fixed once and for all; Λ₀ is the threshold Lam0 of lem:lambda (Paper/Cost.lean).

noncomputable def MIPRE.Halting.semL (G : GapCompression) (U : Cost.UniversalMachine) : Cost.Prog

The search program: the semidecider of 1/2 < val* at level C of the described verifier, from exists_semL.

Equations

• MIPRE.Halting.semL G U = ⋯.choose

theorem MIPRE.Halting.semL_wellScoped (G : GapCompression) (U : Cost.UniversalMachine) : Cost.Prog.WellScoped 1 (semL G U)

theorem MIPRE.Halting.semL_spec (G : GapCompression) (U : Cost.UniversalMachine) (x : Cost.BitStr) : Cost.Halts (semL G U) (Cost.encode x) ↔ 1 / 2 < quantumValue (tabL G U x (C G)).game

noncomputable def MIPRE.Halting.Vpaper (G : GapCompression) (U : Cost.UniversalMachine) (UT : Cost.ClockedUniversalMachine) (M : Cost.Prog) (lam : ℕ) : Verifier 7

The verifier 𝒱^halt M λ with the search program semL.

Equations

• MIPRE.Halting.Vpaper G U UT M lam = MIPRE.Halting.Vhalt G U UT (MIPRE.Halting.semL G U) M lam

noncomputable def MIPRE.Halting.lamThreshold (G : GapCompression) (U : Cost.UniversalMachine) (UT : Cost.ClockedUniversalMachine) : ℕ

The threshold of lem:lambda for the search program semL.

Equations

• MIPRE.Halting.lamThreshold G U UT = MIPRE.Halting.Lam0 G U UT (MIPRE.Halting.semL G U)

theorem MIPRE.Halting.halting_paper (G : GapCompression) (U : Cost.UniversalMachine) (UT : Cost.ClockedUniversalMachine) (M : Cost.Prog) (lam : ℕ) (h : lamThreshold G U UT + 4 * Cost.esize M ≤ lam) : (Cost.Halts M Cost.Data.nil → (Vpaper G U UT M lam).HasPerfectPCC (C G) (Polynomial.eval (C G + lam) G.bound)) ∧ (¬Cost.Halts M Cost.Data.nil → (Vpaper G U UT M lam).valStar (C G) (Polynomial.eval (C G + lam) G.bound) ≤ 1 / 2)

thm:halting, the paper's form: for λ ≥ Λ₀ + 4|M|, at the fixed level C, the game of 𝒱^halt M λ with answers of length at most poly(C, λ) has a value-1 PCC strategy if M halts on the empty input, and value at most 1/2 if it does not.

theorem MIPRE.Halting.halting_paper_valStar (G : GapCompression) (U : Cost.UniversalMachine) (UT : Cost.ClockedUniversalMachine) (M : Cost.Prog) (lam : ℕ) (h : lamThreshold G U UT + 4 * Cost.esize M ≤ lam) : (Cost.Halts M Cost.Data.nil → (Vpaper G U UT M lam).valStar (C G) (Polynomial.eval (C G + lam) G.bound) = 1) ∧ (¬Cost.Halts M Cost.Data.nil → (Vpaper G U UT M lam).valStar (C G) (Polynomial.eval (C G + lam) G.bound) ≤ 1 / 2)

The values of the game, in the form of the criterion route's thm:halting: value 1 if M halts, at most 1/2 if not.