The search program, and the tailored halting theorem without hypothesis

The search program of the tailored halting verifier (SearchSpec, Tailored/Halting/Induction.lean) from the tabulation of a tailored verifier, as MIPRE.Halting.exists_semL gets the existing halting layer's: on a description string x, run the semidecider of 1/2 < val* on the game description toGameData (tabT x C).

• quantumValue_tabT: on the description of a λ-bounded tailored verifier (S^λ, L^λ, P), that game description has the verifier's value at every level n ≥ 2. The tabulation presents the doubled game (presents_tabT), which has no weight on its loops, so it has the doubled game's quantum value (Presents.quantumValue_eq), which is the value of the game (TailoredGame.quantumValue_doubled_eq_valStar); and the conversion to a game description keeps the quantum value (TailoredGameData.quantumValue_toGameData).
• exists_searchProg, search, search_spec: a program meeting the specification at the level C, from the lower semicomputability of the quantum value (exists_semidecider_lt_quantumValue).
• halting_tailored_search: halting_tailored with that program, so with no hypothesis beyond the compression.

theorem MIPRE.Tailored.Halting.quantumValue_tabT {ℓ : ℕ} (TG : TailoredGapCompression ℓ) (lam : ℕ) (P : Decider) (hb : (vof TG lam P).IsBounded lam) {n : ℕ} (hn : 2 ≤ n) : quantumValue (tabT TG (Halting.descOf lam P.prog) n).toGameData.game = (vof TG lam P).valStar n

The tabulated value of a bounded description: on the description of a λ-bounded tailored verifier (S^λ, L^λ, P), at every level n ≥ 2, the game description of its tabulation has the verifier's value.

theorem MIPRE.Tailored.Halting.exists_searchProg {ℓ : ℕ} (TG : TailoredGapCompression ℓ) : ∃ (S' : Cost.Prog), Cost.Prog.WellScoped 1 S' ∧ SearchSpec TG S' (C TG)

A program meeting the search specification at the level C: the semidecider of 1/2 < val* on the tabulation at C of the string it is given.

noncomputable def MIPRE.Tailored.Halting.search {ℓ : ℕ} (TG : TailoredGapCompression ℓ) : Cost.Prog

The search program.

Equations

• MIPRE.Tailored.Halting.search TG = ⋯.choose

theorem MIPRE.Tailored.Halting.search_wellScoped {ℓ : ℕ} (TG : TailoredGapCompression ℓ) : Cost.Prog.WellScoped 1 (search TG)

theorem MIPRE.Tailored.Halting.search_spec {ℓ : ℕ} (TG : TailoredGapCompression ℓ) : SearchSpec TG (search TG) (C TG)

noncomputable def MIPRE.Tailored.Halting.lamThreshold {ℓ : ℕ} (TG : TailoredGapCompression ℓ) (U : Cost.UniversalMachine) (UT : Cost.ClockedUniversalMachine) : ℕ

The threshold of lem:lambda for the search program.

Equations

• MIPRE.Tailored.Halting.lamThreshold TG U UT = MIPRE.Tailored.Halting.Lam0 TG U UT (MIPRE.Tailored.Halting.search TG)

noncomputable def MIPRE.Tailored.Halting.VT {ℓ : ℕ} (TG : TailoredGapCompression ℓ) (U : Cost.UniversalMachine) (UT : Cost.ClockedUniversalMachine) (M : Cost.Prog) (lam : ℕ) : TailoredVerifier ℓ

The tailored halting verifier with the search program.

Equations

• MIPRE.Tailored.Halting.VT TG U UT M lam = MIPRE.Tailored.Halting.Vhalt TG U UT (MIPRE.Tailored.Halting.search TG) M lam

theorem MIPRE.Tailored.Halting.halting_tailored_search {ℓ : ℕ} (TG : TailoredGapCompression ℓ) (U : Cost.UniversalMachine) (UT : Cost.ClockedUniversalMachine) (M : Cost.Prog) (lam : ℕ) (h : lamThreshold TG U UT + 4 * Cost.esize M ≤ lam) : (Cost.Halts M Cost.Data.nil → (VT TG U UT M lam).HasPerfectZPC (C TG)) ∧ (¬Cost.Halts M Cost.Data.nil → (VT TG U UT M lam).valStar (C TG) ≤ 1 / 2)

The tailored halting theorem at a fixed level, from compression alone: for every λ ≥ Λ₀ + 4|M|, at the level C, V^{M,λ} has a perfect ZPC strategy if M halts on the empty input, and value at most 1/2 if it does not.