The tailored halting verifier: the halting theorem at a fixed level #
Paper II, II:2021–2066: the proof of the main theorem from compression, in the form the
halting reduction consumes, along the route of MIPRE/Foundations/Halting/Paper/Main.lean. For
a tailored gap compression TG, a search program S' meeting its specification, every machine
M and every λ ≥ Λ₀ + 4|M|, the tailored verifier V^{M,λ} at the fixed level
C = max C₀ 2 has a perfect ZPC strategy (on the doubled game) if M halts on the empty input,
and value at most 1/2 if it does not.
The level is fixed and the parameter explicit, which is what makes a reduction out of it
polynomial-time: the game is V^{M,λ} at the index C, its sampler and answer-length
calculator are the compressed ones at λ = Λ₀ + 4|M|, and its processor runs within the bound
of Tailored/Halting/Cost.lean.
The search program is a hypothesis (SearchSpec), where the existing halting layer has one at
hand (MIPRE.Halting.semL, from its tabulation): a program meeting it comes from tabulating a
tailored verifier at a fixed level, the next part of the plan.
The tailored halting theorem at a fixed level: for a search program meeting its
specification and 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.
The values, in the form of the halting reduction: value 1 if M halts, at most 1/2 if
not.