The halting reduction, assembled

Blueprint thm:halting: the computable map from machines to game descriptions whose game has value 1 when the machine halts and value at most 1/2 when it does not. It is proved here from gap-preserving compression as a hypothesis (MIPRE.GapCompression, blueprint thm:compression) through the per-level compressibility criterion (MIPRE.Cost.compressibility_criterion_levels, blueprint lem:compressible-criterion), along the dictionary of blueprint rem:compression-abstract.

What a string denotes

A string is a description, never a game: a pair (λ, 𝒟) of a compression parameter and a decider program, serialized by Data.toBitsPost and read back by Data.parse. Every string names such a pair — descLam normalizes the parameter (Data.natOf), descDecD is the decider as the datum it is — so no validity condition on strings appears anywhere. The verifier it denotes is

Vof x = (S^compr_{descLam x}, wrap (descDecD x)) (Verifier.ofSamplerDeciderD),

the compressed sampler at the string's own parameter (which depends on λ alone, blueprint lem:compress-sampler-indep, the field GapCompression.sampler) together with the string's decider, run by the universal machine, wrapped in the question-length check of def:normal-verifier (Decider.wrap). That the decider is a datum and not a decoded program is deliberate: a datum that is not an encoding still names a verifier, whatever the interpreter does with it, and the compressor's decider of O4 can copy a datum into a syntax tree where it could not decode one. The two classes of the criterion are then

classA n = {x | Vof x is n-bounded, rejects long answers, and 𝒱_n has a value-1 PCC strategy}, classB n = {x | Vof x is n-bounded, rejects long answers, and val*(𝒱_n) ≤ 1/2},

with answers cut at ansBound x n = bound (n + descLam x), the length beyond which a compressed decider with parameter descLam x rejects (GapCompression.output_rejects_long); Vof x is not literally an output of Compress, so that field does not apply to it directly — ansBound is the answer alphabet the classes are read with, and relating it to the compressor's output is part of Obligations.compr_spec. Tying the boundedness parameter to the level (n-bounded at level n) is what replaces the paper's choice of λ along the recursion (blueprint rem:compression-abstract, item 1, and lem:lambda).

Where the assembly is

halting_reduction, and the structure MIPRE.Halting.Obligations of what it still owes, are in Halting/Reduction.lean, which sits below this file, Halting/Strings.lean and Halting/Semidecider.lean in the import order, so that the two distinguished strings (O1) and the semidecider (O3) are applied there as theorems rather than assumed as fields. What this file contributes to it, beyond the objects above, is the tabulation:

• O2 — the tabulation of 𝒱_n as a game description matching it along relabelings of the two alphabets: tab, tab_computable, tab_match, tab_value and gameValue_tab_eq_one, in the last section of this file, which halting_reduction uses directly; the relabelings are Verifier.tagEquiv and answerEquiv, transported across the two sizes. Three features of their shape are deliberate and each is explained where it is stated: the match and the value hold of an n-bounded verifier and could not hold of every string, acceptance being Σ₁ — while dimOf_eq and margOf_eq, budgeted from the compressed sampler's own time bound, hold at every string and every level; tab_match delivers the relabelings rather than only the value they equate, because synval ≤ val* points the wrong way for item 1 of thm:halting; and the game it matches is the doubled one, (Vof G U x).doubledGame, so that the diagonal a GameData vetoes carries no weight and no synchronicity is asked of the verifier. That last one is what makes the tabulation usable by O3, and the paragraph below the list says how.

O3 was recorded in planning/h4-assembly.md as "O2 plus a disjunction"; it is not, and the reason is worth naming, because it shaped the tabulation. Halting.exists_sem_of_tab needs the tabulation to have the value of 𝒱_n at every n-bounded string, in both directions, because sem_spec is an equivalence — while a match against (Vof G U x).game gives that only where the verifier is also synchronous at n, a GameData describing a synchronous game by construction (Verifier.isSynchronousAt_of_game_matches), and classB n does not ask for synchronicity. Three repairs were on the record in blueprint lem:halting-semidecider: tabulate on a doubled question set so that the distribution avoids the diagonal, make Decider.wrap reject unequal answers to equal questions so that every string names a synchronous verifier, or put synchronicity into classB and pay for it in compr_spec. The first is the one made (Foundations/GameDouble.lean, Verifier.doubledGame): it is the cheapest and the only one that changes nothing outside the tabulation. So tab_match and tab_value below ask the verifier's decider for nothing beyond n-boundedness, and exists_sem_of_tab's hval is tab_value itself.

What a string denotes

def MIPRE.Halting.descLam (x : Cost.BitStr) : ℕ

The compression parameter a string denotes: the left component of the data it parses to, normalized to a canonical binary numeral (Data.natOf), so that every string names one.

Equations

• MIPRE.Halting.descLam x = (MIPRE.Cost.Data.parse x).left.natOf

def MIPRE.Halting.descDecD (x : Cost.BitStr) : Cost.Data

The decider a string denotes: the right component of the data it parses to, a datum that the universal machine runs (Verifier.ofSamplerDeciderD). It need not be the encoding of a program; every string names one.

Equations

• MIPRE.Halting.descDecD x = (MIPRE.Cost.Data.parse x).right

def MIPRE.Halting.descOf (lam : ℕ) (dec : Cost.Prog) : Cost.BitStr

The string denoting a parameter and a decider: the postorder serialization of the pair.

Equations

• MIPRE.Halting.descOf lam dec = ((MIPRE.Cost.encode lam).cons (MIPRE.Cost.encode dec)).toBitsPost

@[simp]

theorem MIPRE.Halting.descLam_descOf (lam : ℕ) (dec : Cost.Prog) : descLam (descOf lam dec) = lam

@[simp]

theorem MIPRE.Halting.descDecD_descOf (lam : ℕ) (dec : Cost.Prog) : descDecD (descOf lam dec) = Cost.encode dec

The verifier a string denotes, and the two classes

def MIPRE.Halting.Vof (G : GapCompression) (U : Cost.UniversalMachine) (x : Cost.BitStr) : Verifier 7

The verifier a string denotes: the compressed sampler at the string's own parameter, and the string's decider — a datum, run by the universal machine — wrapped in the question-length check. Every string denotes one, well formed or not.

Equations

• MIPRE.Halting.Vof G U x = MIPRE.Verifier.ofSamplerDeciderD U (G.sampler (MIPRE.Halting.descLam x)) (MIPRE.Halting.descDecD x)

def MIPRE.Halting.ansBound (G : GapCompression) (x : Cost.BitStr) (n : ℕ) : ℕ

The answer-length budget the classes are read with at level n: the bound a compressed decider with the string's parameter obeys at index n.

Equations

• MIPRE.Halting.ansBound G x n = Polynomial.eval (n + MIPRE.Halting.descLam x) G.bound

The answer budget of a short description

What obligation O4 needs of ansBound: on a string short enough to have come out of the compressibility criterion, the budget the classes are read with at level 2n + 1 is below the budget GapCompression.completeness supplies strategies at. Both bounds are exponential in n; the point is which exponent, and the string's own parameter is what could have broken it.

theorem MIPRE.Halting.descLam_lt (x : Cost.BitStr) : descLam x < 2 ^ max 1 (List.length x)

A string denotes a parameter exponential in its length at worst. The parameter is the number the left component of the parsed datum denotes, and parsing a string of length L yields a datum of size at most L (Data.size_parse_le), which denotes a number below 2 ^ L (Data.natOf_lt).

theorem MIPRE.Halting.descLam_lt_of_length_le {x : Cost.BitStr} {n : ℕ} (h : List.length x ≤ n + 1) : descLam x < 2 ^ (n + 1)

The form the criterion's length bound is used in: compr_spec's hypothesis x.length ≤ n + 1 caps the denoted parameter at 2 ^ (n + 1).

theorem MIPRE.Halting.exists_ansBound_le (G : GapCompression) : ∃ (lam₀ : ℕ) (n₀ : ℕ), ∀ (x : Cost.BitStr) (lam n : ℕ), lam₀ ≤ lam → n₀ ≤ n → List.length x ≤ n + 1 → ansBound G x (2 * n + 1) ≤ (2 ^ n) ^ lam

The answer budget of level 2n + 1 fits under the compression theorem's. For λ and n above thresholds depending only on G.bound, a string of length at most n + 1 has ansBound G x (2n+1) ≤ (2 ^ n) ^ λ --- the budget at which GapCompression.completeness takes its hypothesis. With Verifier.hasPerfectPCC_of_le this is what carries a value-1 PCC strategy from membership in classA G U (2 * n + 1) into that clause, and it is why Obligations.compr_spec carries the length bound: ansBound grows with the string's own parameter, so without it no pair of thresholds would do.

The thresholds are λ ≥ 2 · deg(bound) + 1 and n ≥ log₂(‖bound‖) + 2 · deg(bound) + 1, where ‖bound‖ is the sum of its coefficients; note they are set by the polynomial bound, not by G.deg, which grades running times in the input size instead.

def MIPRE.Halting.classA (G : GapCompression) (U : Cost.UniversalMachine) (n : ℕ) : Set Cost.BitStr

The class A at level n: the strings whose verifier is n-bounded and whose n-th game has a value-1 PCC strategy.

Equations

• MIPRE.Halting.classA G U n = {x : MIPRE.Cost.BitStr | (MIPRE.Halting.Vof G U x).InClassA n (MIPRE.Halting.ansBound G x n)}

def MIPRE.Halting.classB (G : GapCompression) (U : Cost.UniversalMachine) (ω : ValueModel) (n : ℕ) : Set Cost.BitStr

The class B at level n, in the value model ω: the strings whose verifier is n-bounded, rejects long answers, and whose n-th game has value at most 1/2 in the model. At ValueModel.tensor this is the class of the halting reduction of MIP* = RE; at ValueModel.commuting, the one of MIP^co = coRE.

Equations

• MIPRE.Halting.classB G U ω n = {x : MIPRE.Cost.BitStr | (MIPRE.Halting.Vof G U x).InClassB ω n (MIPRE.Halting.ansBound G x n)}

theorem MIPRE.Halting.mem_classB_iff (G : GapCompression) (U : Cost.UniversalMachine) {ω : ValueModel} {n : ℕ} {x : Cost.BitStr} : x ∈ classB G U ω n ↔ (Vof G U x).InClassB ω n (ansBound G x n)

theorem MIPRE.Halting.notMem_classB_of_mem_classA (G : GapCompression) (U : Cost.UniversalMachine) {ω : ValueModel} {n : ℕ} {x : Cost.BitStr} (h : x ∈ classA G U n) : x ∉ classB G U ω n

The two classes are disjoint at every level: a perfect PCC strategy gives value 1.

The tabulation of the verifier a string denotes

tab x n is the GameData for (Vof G U x)'s n-th game, and it is computable because it is Tabulate's tabOf — a function of two encoded programs and five numbers — fed what the string and the level supply: the two programs, the sampler's dimension, the answer cut ansBound G x n, and that same ansBound with G.deg as the budget of the sampler runs. Two of the seven take work:

• sampData x, the encoded sampler program, is G.samplerProg (descLam x) encoded. A PolyTimeFun is not a Mathlib-computable function of its argument in any direct sense; what makes this go through is that it is run by the ambient machine on an encoded input (Cost.PolyTimeFun.computable_encode_comp).
• decProgData x, the encoded decider program, is the wrapper around the string's own decider (Decider.wrap, through Verifier.ofSamplerDecider). Encoding it means building Cost.Prog.wrapCore's syntax tree directly in Data (Cost.Prog.ProgD.dWrapCore), because Prog is not a Primcodable and so no Primrec statement can mention it. The string's decider is the datum descDecD x and enters as it is.

The three bridges at the end — accOf_iff, dimOf_eq, margOf_eq — are what the rest of O2 rests on: the tabulated numbers are the verifier's own sampler and decider. dimOf_eq and margOf_eq say so at every string and every level, their budget being the compressed sampler's own (sampler_timeBound, from GapCompression.sampler_time); accOf_iff says so on an n-bounded verifier, whose budget is the only one the string's own decider has.

def MIPRE.Halting.sampData (G : GapCompression) (x : Cost.BitStr) : Cost.Data

The encoded sampler program of the verifier a string denotes.

Equations

• MIPRE.Halting.sampData G x = MIPRE.Cost.encode (G.samplerProg.toFun (MIPRE.Halting.descLam x))

def MIPRE.Halting.decProgData (G : GapCompression) (U : Cost.UniversalMachine) (x : Cost.BitStr) : Cost.Data

The encoded decider program of the verifier a string denotes: the question-length wrapper around the string's decider, built in Data rather than in Prog.

Equations

• MIPRE.Halting.decProgData G U x = MIPRE.Cost.Prog.ProgD.dWrapCore (MIPRE.Cost.encode U.univ) (MIPRE.Halting.sampData G x) (MIPRE.Halting.descDecD x)

The two concrete instantiations of Tabulate's generic Primrec statements. s and B are paired so that n stays at the depth it has in the tuple today: that is what keeps this one instantiation cheap, and what lets tabOf's argument list grow without re-running the expensive primrec_accOf.

theorem MIPRE.Halting.primrec_dimOf_tuple (k : ℕ) : Primrec fun (q : (Cost.Data × ℕ) × ℕ) => dimOf q.1.1 q.2 k q.1.2

theorem MIPRE.Halting.primrec_tabOf_tuple (k : ℕ) : Primrec fun (q : (Cost.Data × Cost.Data) × (ℕ × ℕ) × ℕ × ℕ) => tabOf q.1.1 q.1.2 q.2.1.1 q.2.2.1 q.2.1.2 k q.2.2.2

noncomputable def MIPRE.Halting.tab (G : GapCompression) (U : Cost.UniversalMachine) (x : Cost.BitStr) (n : ℕ) : HaltingGameValue.GameData

The tabulation of (Vof G U x)'s n-th game, doubled and re-budgeted. The sampler runs under the budget the compressed sampler's own time bound supplies — coefficient ansBound G x n = G.bound.eval (n + descLam x), degree G.deg — neither of which needs (Vof G U x).IsBounded n.

Equations

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

The tabulation is computable

theorem MIPRE.Halting.primrec_descLam : Primrec descLam

theorem MIPRE.Halting.computable_sampData (G : GapCompression) : Computable fun (x : Cost.BitStr) => sampData G x

theorem MIPRE.Halting.computable_decProgData (G : GapCompression) (U : Cost.UniversalMachine) : Computable fun (x : Cost.BitStr) => decProgData G U x

theorem MIPRE.Halting.computable_ansBound (G : GapCompression) : Computable fun (p : Cost.BitStr × ℕ) => ansBound G p.1 p.2

The seven arguments of tabOf are assembled one declaration at a time. Inlining them into a single term is not a stylistic choice: the tuple is nested four deep and elaborating it in one go does not terminate within any heartbeat budget worth setting.

theorem MIPRE.Halting.computable_sampData_fst (G : GapCompression) : Computable fun (p : Cost.BitStr × ℕ) => sampData G p.1

theorem MIPRE.Halting.computable_decProgData_fst (G : GapCompression) (U : Cost.UniversalMachine) : Computable fun (p : Cost.BitStr × ℕ) => decProgData G U p.1

theorem MIPRE.Halting.computable_dimOf_fst (G : GapCompression) : Computable fun (p : Cost.BitStr × ℕ) => dimOf (sampData G p.1) (ansBound G p.1 p.2) G.deg p.2

theorem MIPRE.Halting.computable_tabArgs (G : GapCompression) (U : Cost.UniversalMachine) : Computable fun (p : Cost.BitStr × ℕ) => ((sampData G p.1, decProgData G U p.1), (dimOf (sampData G p.1) (ansBound G p.1 p.2) G.deg p.2, ansBound G p.1 p.2), ansBound G p.1 p.2, p.2)

theorem MIPRE.Halting.tab_computable (G : GapCompression) (U : Cost.UniversalMachine) : Computable fun (p : Cost.BitStr × ℕ) => tab G U p.1 p.2

O2, computability.

The tabulated numbers are the verifier's own

sampData_eq and decProgData_eq only unfold the two encodings, and hold at every n. The other three — accOf_iff, dimOf_eq, margOf_eq — are the same shape: rewrite the budgeted run into CL.Sampler.queryUnder or Verifier.accepts_iff_runForD, which a time bound then evaluates. Which bound differs, and that is the point of the re-budget. The two sampler runs take sampler_timeBound — GapCompression.sampler_time at the string's own parameter, a bound at every index — so dimOf_eq and margOf_eq carry no hypothesis. accOf_iff has only IsBounded n to draw on, and IsBounded.two_le supplies the 2 ≤ n it needs — see the warning there: at n = 0, 1 the time clauses say nothing and no budget exists.

theorem MIPRE.Halting.sampData_eq (G : GapCompression) (x : Cost.BitStr) : sampData G x = Cost.encode (G.sampler (descLam x)).prog

theorem MIPRE.Halting.decProgData_eq (G : GapCompression) (U : Cost.UniversalMachine) (x : Cost.BitStr) : decProgData G U x = Cost.encode (Vof G U x).decider.prog

theorem MIPRE.Halting.accOf_iff (G : GapCompression) (U : Cost.UniversalMachine) (x : Cost.BitStr) (n : ℕ) (hb : (Vof G U x).IsBounded n) (x' y' a b : Cost.BitStr) : accOf (decProgData G U x) n x' y' a b = true ↔ (Vof G U x).decider.Accepts n x' y' a b

The tabulated acceptance test is the verifier's acceptance, on an n-bounded verifier.

theorem MIPRE.Halting.sampler_timeBound (G : GapCompression) (x : Cost.BitStr) (n : ℕ) : (G.sampler (descLam x)).TimeBoundAt n (ansBound G x n) G.deg

The sampler's time bound at the string's own compression parameter, with no hypothesis.

theorem MIPRE.Halting.dimOf_eq (G : GapCompression) (U : Cost.UniversalMachine) (x : Cost.BitStr) (n : ℕ) : dimOf (sampData G x) (ansBound G x n) G.deg n = (Vof G U x).sampler.dim n

The tabulated dimension is the sampler's, at every string and every level — n = 0 and n = 1 included, which the n ^ n budget could never reach.

theorem MIPRE.Halting.margOf_eq (G : GapCompression) (U : Cost.UniversalMachine) (x : Cost.BitStr) (n : ℕ) (w : Player) (z : Cost.BitStr) (hz : List.length z = (Vof G U x).sampler.dim n) : margOf (sampData G x) (ansBound G x n) G.deg n w z = CL.toBits (((Vof G U x).sampler.cl n w).eval (CL.ofBits ((Vof G U x).sampler.dim n) z))

The tabulated marginal is the sampler's, at every string and every level. The only remaining hypothesis is the length condition on the point, which is not a boundedness one.

The tabulation matches the verifier, doubled

What remains is the dictionary between the two namings of each alphabet. A GameData names its questions Fin (nX + 1) and its answers Fin (nA + 1); the doubled game names them Bool × 𝔽₂^{s(n)} and the bit strings of length at most T. Verifier.tagEquiv and Verifier.answerEquiv are the two bijections, and eXof/eAof are them transported across the arithmetic of tab's two sizes (tab_nX, tab_nA) — nX + 1 = 2 ^ (s(n) + 1), the extra bit being the tag.

The two clauses are then separate pieces of work. The μ clause (mu_clause) is a counting argument: the tabulated weight of a question pair is the number of points of 𝔽₂^{s(n)} whose two tagged marginals land on it, and the total weight is still 2 ^ s(n), which is exactly the quotient CL.clDist is — the weight list enumerates 𝔽₂^{s(n)} once, not the strings of length s(n) + 1. The D clause is the acceptance table read back (acc_mem_iff), and the one place where the two notions of game differ has stopped costing anything: a GameData rejects unequal answers to equal questions by construction, and the doubled game puts no weight there and rejects there too, so tab_match is a total match and needs nothing of the decider beyond n-boundedness.

theorem MIPRE.Halting.tab_nX (G : GapCompression) (U : Cost.UniversalMachine) (x : Cost.BitStr) (n : ℕ) : (tab G U x n).nX + 1 = 2 ^ ((Vof G U x).sampler.dim n + 1)

theorem MIPRE.Halting.tab_nA (G : GapCompression) (U : Cost.UniversalMachine) (x : Cost.BitStr) (n : ℕ) : (tab G U x n).nA + 1 = (Verifier.answerList (ansBound G x n)).length

noncomputable def MIPRE.Halting.eXof (G : GapCompression) (U : Cost.UniversalMachine) (x : Cost.BitStr) (n : ℕ) : Fin ((tab G U x n).nX + 1) ≃ Bool × (Vof G U x).Questions n

The question relabeling: a tabulated question index is a tag and a point of 𝔽₂^{s(n)}.

Equations

• MIPRE.Halting.eXof G U x n = (finCongr ⋯).trans (MIPRE.Verifier.tagEquiv ((MIPRE.Halting.Vof G U x).sampler.dim n)).symm

noncomputable def MIPRE.Halting.eAof (G : GapCompression) (U : Cost.UniversalMachine) (x : Cost.BitStr) (n : ℕ) : Fin ((tab G U x n).nA + 1) ≃ Verifier.Answers (ansBound G x n)

The answer relabeling: a tabulated answer index is a bit string of length at most the answer bound. Only the questions are doubled, so this is unchanged by it.

Equations

• MIPRE.Halting.eAof G U x n = (finCongr ⋯).trans (MIPRE.Verifier.answerEquiv (MIPRE.Halting.ansBound G x n))

theorem MIPRE.Halting.eXof_apply (G : GapCompression) (U : Cost.UniversalMachine) (x : Cost.BitStr) (n : ℕ) (i : Fin ((tab G U x n).nX + 1)) : Verifier.bitsToIdx (((eXof G U x n) i).1 :: CL.toBits ((eXof G U x n) i).2) = ↑i

theorem MIPRE.Halting.eAof_apply (G : GapCompression) (U : Cost.UniversalMachine) (x : Cost.BitStr) (n : ℕ) (k : Fin ((tab G U x n).nA + 1)) : List.idxOf (↑((eAof G U x n) k)) (Cost.Data.bitStrsLE (ansBound G x n)) = ↑k

theorem MIPRE.Halting.marg_idx_eq (G : GapCompression) (U : Cost.UniversalMachine) (x : Cost.BitStr) (n : ℕ) (w : Player) (tg : Bool) (z : Cost.BitStr) (hz : List.length z = (Vof G U x).sampler.dim n) (i : Fin ((tab G U x n).nX + 1)) : Verifier.bitsToIdx (tg :: margOf (sampData G x) (ansBound G x n) G.deg n w z) = ↑i ↔ tg = ((eXof G U x n) i).1 ∧ ((Vof G U x).sampler.cl n w).eval (CL.ofBits ((Vof G U x).sampler.dim n) z) = ((eXof G U x n) i).2

The dictionary the μ clause runs on, with the tag: a tagged marginal lands on the index i exactly when the tag is i's tag and the verifier's own marginal is i's point.

theorem MIPRE.Halting.mu_clause (G : GapCompression) (U : Cost.UniversalMachine) (x : Cost.BitStr) (n : ℕ) (i j : Fin ((tab G U x n).nX + 1)) : (tab G U x n).game.μ i j = ((Vof G U x).doubledGame n (ansBound G x n)).μ ((eXof G U x n) i) ((eXof G U x n) j)

The μ clause, doubled. The tabulated distribution is the sampler's on the block (false, ·) × (true, ·) and zero everywhere else — which is exactly the doubled game's.

theorem MIPRE.Halting.acc_mem_iff (G : GapCompression) (U : Cost.UniversalMachine) (x : Cost.BitStr) (n : ℕ) (hb : (Vof G U x).IsBounded n) (i j : Fin ((tab G U x n).nX + 1)) (k l : Fin ((tab G U x n).nA + 1)) : (↑i, ↑j, ↑k, ↑l) ∈ (tab G U x n).acc ↔ ((eXof G U x n) i).1 = false ∧ ((eXof G U x n) j).1 = true ∧ (Vof G U x).decider.Accepts n (CL.toBits ((eXof G U x n) i).2) (CL.toBits ((eXof G U x n) j).2) ↑((eAof G U x n) k) ↑((eAof G U x n) l)

The acceptance table read back, doubled. A tuple of indices is in the table exactly when the tags are Alice's and Bob's and the verifier's decider accepts.

theorem MIPRE.Halting.tab_match (G : GapCompression) (U : Cost.UniversalMachine) (x : Cost.BitStr) (n : ℕ) (hb : (Vof G U x).IsBounded n) : ∃ (eX : Fin ((tab G U x n).nX + 1) ≃ Bool × (Vof G U x).Questions n) (eA : Fin ((tab G U x n).nA + 1) ≃ Verifier.Answers (ansBound G x n)), (∀ (i j : Fin ((tab G U x n).nX + 1)), (tab G U x n).game.μ i j = ((Vof G U x).doubledGame n (ansBound G x n)).μ (eX i) (eX j)) ∧ ∀ (i j : Fin ((tab G U x n).nX + 1)) (k l : Fin ((tab G U x n).nA + 1)), (tab G U x n).game.D i j k l = ((Vof G U x).doubledGame n (ansBound G x n)).D (eX i) (eX j) (eA k) (eA l)

O2, the match — doubled, and with no synchronicity hypothesis. On an n-bounded verifier the doubled tabulation matches the doubled game of 𝒱_n along eXof and eAof. The forced rejections of a GameData sit on the diagonal, which the doubled distribution avoids; and the doubled game rejects off the tag block, which is what the table omits.

theorem MIPRE.Halting.tab_val (G : GapCompression) (U : Cost.UniversalMachine) (ω : ValueModel) (x : Cost.BitStr) (n : ℕ) (hb : (Vof G U x).IsBounded n) : ω.val (tab G U x n).game = (Vof G U x).val ω n (ansBound G x n)

O2, the value — doubled, in any model: the tabulated game has the value of 𝒱_n in every value model at every n-bounded string, with no synchronicity hypothesis. This is Halting.exists_sem_of_tab's hval.

theorem MIPRE.Halting.tab_value (G : GapCompression) (U : Cost.UniversalMachine) (x : Cost.BitStr) (n : ℕ) (hb : (Vof G U x).IsBounded n) : quantumValue (tab G U x n).game = (Vof G U x).valStar n (ansBound G x n)

O2, the value — doubled: the tabulated game has the quantum value of 𝒱_n at every n-bounded string.

def MIPRE.Halting.classOne (G : GapCompression) (U : Cost.UniversalMachine) (ω : ValueModel) (n : ℕ) : Set Cost.BitStr

The class of value 1 at level n, in the value model ω, read on the tabulation: the strings whose tabulated game at level n (tab, below) does not have value below 1. The larger of the two nested classes of the coRE direction (Cost.compressibility_criterion_nested, planning/mipco-track.md §3): its complement is what an upper semidecider for the value recognizes, and it contains classA (classA_subset_classOne). It is read on the tabulation directly so that the non-halting conclusion of the criterion needs no boundedness.

Equations

• MIPRE.Halting.classOne G U ω n = {x : MIPRE.Cost.BitStr | ¬ω.val (MIPRE.Halting.tab G U x n).game < 1}

theorem MIPRE.Halting.mem_classOne_iff (G : GapCompression) (U : Cost.UniversalMachine) {ω : ValueModel} {n : ℕ} {x : Cost.BitStr} : x ∈ classOne G U ω n ↔ ¬ω.val (tab G U x n).game < 1

theorem MIPRE.Halting.val_tab_eq_one_of_mem_classOne (G : GapCompression) (U : Cost.UniversalMachine) {ω : ValueModel} {n : ℕ} {x : Cost.BitStr} (h : x ∈ classOne G U ω n) : ω.val (tab G U x n).game = 1

In classOne the tabulated game has value exactly 1.

theorem MIPRE.Halting.classA_subset_classOne (G : GapCompression) (U : Cost.UniversalMachine) (ω : ValueModel) (n : ℕ) : classA G U n ⊆ classOne G U ω n

The perfect-PCC class lies in the class of value 1 of every model: a perfect PCC strategy gives val* = 1, and every model dominates val*. This is the nesting B₀ ⊆ B₁ of Cost.compressibility_criterion_nested.

theorem MIPRE.Halting.gameValue_tab_eq_one (G : GapCompression) (U : Cost.UniversalMachine) (x : Cost.BitStr) (n : ℕ) (hb : (Vof G U x).IsBounded n) (hV : (Vof G U x).HasPerfectPCC n (ansBound G x n)) : HaltingGameValue.gameValue (tab G U x n).toGame = 1

The completeness branch, in the value of HaltingGameValue.