The two distinguished strings

Obligation O1 of the halting reduction (Halting/Reduction.lean, which applies yYes_mem and yNo_mem directly): a string whose verifier lies in classA n at every level above a threshold, and one whose verifier lies in classB n.

Both are descriptions descOf 0 𝒟 with the compressed sampler at parameter 0 and a decider program of three or four nodes:

• decNo is the program nil. Its result is nil, never encode true, so the wrapped decider accepts nothing, the verifier is synchronous at every index for want of an accepting tuple, and val* = 0 (Verifier.inClassB_of_rejects_all).
• decYes takes the input (n, x, y, a, b) apart and returns encode true exactly when both answers are the empty string. The paper's halting case is a decider that accepts everything; in the synchronous framework that verifier is not synchronous at all — equal questions with unequal answers must be rejected — so the fixed-answer form is what item 1 of thm:halting takes here (Verifier.inClassA_of_accepts_diagonal, the paper's trivial strategy).

λ-boundedness of both comes from Verifier.ofSamplerDecider_isBounded, whose three hypotheses are fields of MIPRE.GapCompression for the sampler and immediate for these two programs, each of which halts at constant cost.

The two decider programs

def MIPRE.Halting.decNo : Cost.Prog

The rejecting decider: the program nil, which returns nil on every input.

Equations

• MIPRE.Halting.decNo = MIPRE.Cost.Prog.nil

def MIPRE.Halting.decYes : Cost.Prog

The fixed-answer decider: on (n, x, y, a, b) it returns encode true exactly when a and b are both the empty bit string. Four elims take the tuple apart and two more test the answers.

Equations

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

theorem MIPRE.Halting.decNo_runs (v : Cost.Data) : decNo.Runs v Cost.Data.nil 1

theorem MIPRE.Halting.decNo_hasPolyCost : decNo.HasPolyCost

theorem MIPRE.Halting.decNo_not_runs_true (v : Cost.Data) (t : ℕ) : ¬decNo.Runs v (Cost.encode true) t

The rejecting decider never returns encode true.

The fixed-answer decider

theorem MIPRE.Halting.decYes_run_deep (A B C D E : Cost.Data) : ∃ t ≤ 10, decYes.Runs (A.cons (B.cons (C.cons (D.cons E)))) (if D = Cost.Data.nil ∧ E = Cost.Data.nil then Cost.encode true else Cost.Data.nil) t

On an input with at least four nodes on its right spine — the shape of a well-formed tuple (n, x, y, a, b) — decYes returns encode true exactly when the last two components are both nil.

theorem MIPRE.Halting.decYes_halts (v : Cost.Data) : ∃ (r : Cost.Data), ∃ t ≤ 10, decYes.Runs v r t

decYes halts on every input, well formed or not, at constant cost: each of its elims either returns nil at once or descends one node.

theorem MIPRE.Halting.decYes_hasPolyCost : decYes.HasPolyCost

theorem MIPRE.Halting.decYes_runs_true_iff (n : ℕ) (x y a b : Cost.BitStr) : (∃ (t : ℕ), decYes.Runs (Cost.encode (n, x, y, a, b)) (Cost.encode true) t) ↔ a = [] ∧ b = []

What decYes accepts: the empty answer from both players, on every question pair.

The compressed sampler

theorem MIPRE.Halting.sampler_hasPolyCost (G : GapCompression) (lam : ℕ) : (G.sampler lam).prog.HasPolyCost

The compressed sampler's cost is polynomially bounded: its time bound is bound (n + λ) at the fixed degree deg (GapCompression.sampler_time).

theorem MIPRE.Halting.sampler_polyBounded_dim (G : GapCompression) (lam : ℕ) : Cost.PolyBounded (G.sampler lam).dim

Its dimension is polynomially bounded (GapCompression.sampler_dim).

The two strings

def MIPRE.Halting.yNo : Cost.BitStr

The string of the class B: parameter 0, decider nil.

Equations

• MIPRE.Halting.yNo = MIPRE.Halting.descOf 0 MIPRE.Halting.decNo

def MIPRE.Halting.yYes : Cost.BitStr

The string of the class A: parameter 0, the fixed-answer decider.

Equations

• MIPRE.Halting.yYes = MIPRE.Halting.descOf 0 MIPRE.Halting.decYes

@[simp]

theorem MIPRE.Halting.Vof_yNo (G : GapCompression) (U : Cost.UniversalMachine) : Vof G U yNo = Verifier.ofSamplerDecider U (G.sampler 0) decNo

@[simp]

theorem MIPRE.Halting.Vof_yYes (G : GapCompression) (U : Cost.UniversalMachine) : Vof G U yYes = Verifier.ofSamplerDecider U (G.sampler 0) decYes

theorem MIPRE.Halting.yNo_mem (G : GapCompression) (U : Cost.UniversalMachine) (ω : ValueModel) : ∃ (n₀ : ℕ), ∀ (n : ℕ), n₀ ≤ n → yNo ∈ classB G U ω n

O1, the rejecting side. yNo lies in the class B of every value model at every level from some n₀ on: its verifier accepts nothing, hence is synchronous and has value 0, and it is n-bounded above the threshold of Verifier.ofSamplerDecider_isBounded.

theorem MIPRE.Halting.yYes_mem (G : GapCompression) (U : Cost.UniversalMachine) : ∃ (n₀ : ℕ), ∀ (n : ℕ), n₀ ≤ n → yYes ∈ classA G U n

O1, the accepting side. yYes lies in the class A at every level from some n₀ on: its verifier accepts the empty answer from both players on every question pair and nothing else, so the constant strategy is a value-1 PCC strategy and every long answer is rejected.