The abstract compression lemmas

Two abstract compression lemmas, each turning a compression procedure on succinct descriptions into a reduction from the halting problem, together with their halting-problem corollaries in the form consumed by MIPRE.HaltingGameValue:

• recursive_compression: the lemma of Marks–Nezhadi–Yuen ("The recursive compression method for proving undecidability results"), in the variant with compression parameter n ([MNY, Lemma 5.1]) — blueprint lem:recursive-compression — whose hypothesis is the growth of a measure f (the entanglement requirement, in the pipeline of [JNVWY]);
• compressibility_criterion: Lin's compression criterion (MIP^co = coRE) — blueprint lem:compressible-criterion — whose hypothesis is the preservation of two classes, in value form, plus the semidecidability of the complement of the second. This is the lemma the value-form pipeline of the blueprint uses. The adapted notion of succinct description (blueprint def:succinct, [MNY, Definition 2.4]) is Cost.IsSuccinctDesc in Cost/Succinct.lean.

Everything is stated in the ambient cost model (Cost.Basic): programs are Cost.Prog, "polynomial-time computable" is Cost.PolyTimeFun, runtimes are Cost.Eval. The proof is the fixed-point construction of [MNY, Lemma 3.1/5.1] and uses precisely the toolkit of Cost.Toolkit: hardcode (efficient s-m-n) and PolyTimeFun.smn to build the self-referential decider, a ClockedUniversalMachine to run "e for log n steps" (PolyTimeFun.haltsWithin), a UniversalMachine to answer bit-queries within the succinctness budget (Prog.bitQueryProg), and efficient_fixed_point to close the self-reference; the time-transfer clauses are what make the constructed program a succinct description at every recursion level (planning/compression-track.md, K3).

Departures from the paper's statement and proof

• Succinctness time bound. [MNY, Definition 2.4] requires runtime(e, m) ≤ n for all m. In any cost model that charges to read its input (ours does), that bound is vacuous for |m| > n; we require ≤ (n + 1) * (Nat.size m + 1) ^ 2 instead. Any poly(n, |m|) bound would do; the choice only shifts polynomial overheads inside the proof, but it must be fixed consistently with the compression theorem for games (thm:compression) whose output verifiers are what get succinctly described. The quadratic factor in |m| is what the bit-query program Cost.Prog.bitAtProg achieves: in the list language, a zero test or a decrement of the binary index copies the index, so each of the |y| steps of the walk costs O(size y + |m| ^ 2) (Cost.Prog.bitAtIter_le). Design knob (K-D5) — revisit when thm:compression is stated.
• The next level is 2 n + 1, not n + 1. The paper's decider at level n compresses a description of the string at level n + 1. Incrementing a binary numeral needs a carry propagation; prepending a true bit is one node (PolyTimeFun.next). The argument is unchanged: the levels n, 2n + 1, 4n + 3, … still grow without bound, and Nat.size (2 n + 1) = Nat.size n + 1 keeps every overhead polynomial in esize e + Nat.size n.
• The threshold is r e = 2 ^ (K + 1 + esize e) for a constant K obtained from the overhead polynomial by exists_threshold (Cost/Growth.lean): above it, the polynomial overhead in esize e + Nat.size n is at most n + 1. It is computed by PolyTimeFun.threshold K.
• The instantiation (blueprint rem:compression-abstract) uses the per-level form compressibility_criterion_levels: A n = descriptions of n-bounded normal form verifiers whose n-th game has a value-1 PCC strategy, B n = those with value at most 1/2 at index n, and S = the enumeration of strategies of value above 1/2 (blueprint lem:value-lower-approx, MIPRE.exists_semidecider_lt_quantumValue) on the tabulated n-th game. The compressor cannot read the succinct description it is handed — a bit query costs up to n, its own time is polylogarithmic in n — so it embeds the description into a decider that reads it at game time, with the verifier it describes frozen at index 2n + 1; that is what the size slack 2 · |c| ≤ n and the level bookkeeping of the per-level form are for. For recursive_compression, f = MIPRE.entRequirement (·, 1/2) : _ → ℕ∞; the ℕ∞ codomain there matches entRequirement.

The self-referential decider

noncomputable def MIPRE.Cost.decFun (U : UniversalMachine) (UT : ClockedUniversalMachine) (Compr : PolyTimeFun ((Prog × ℕ) × ℕ) BitStr) (y₀ : BitStr) : PolyTimeFun (Prog × Prog × ℕ) BitStr

The decider of the recursive compression argument, as a polynomial-time function of (c', (e, n)): if e halts on the empty input within Nat.size n steps, the fixed string y₀; otherwise Compr applied to the succinct description (hardcode β ((c', e), 2n + 1), n) — where β is the bit-query program — with parameter n. The self-referential program c of the proof is a Kleene fixed point of c' ↦ hardcode (decFun …).code (encode c'), so that c on (e, n) computes decFun (c, (e, n)), and the hardcoded description is of the string that c itself computes at the next level.

Equations

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

theorem MIPRE.Cost.decFun_apply (U : UniversalMachine) (UT : ClockedUniversalMachine) (Compr : PolyTimeFun ((Prog × ℕ) × ℕ) BitStr) (y₀ : BitStr) (c' e : Prog) (n : ℕ) : (decFun U UT Compr y₀).toFun (c', e, n) = if (evalWithin e Data.nil n.size).isSome = true then y₀ else Compr.toFun ((hardcode U.univ.bitQueryProg (encode ((c', e), 2 * n + 1)), n), n)

The compression lemma

theorem MIPRE.Cost.recursive_compression (f : BitStr → ℕ∞) (A : Set BitStr) (y₀ : BitStr) (hy₀ : y₀ ∈ A) (_hA : ∀ x ∈ A, f x < ⊤) (Compr : PolyTimeFun ((Prog × ℕ) × ℕ) BitStr) (hCompr : ∀ (c : Prog) (m : ℕ) (x : BitStr) (n : ℕ), IsSuccinctDesc c m x → max (f x) ↑n ≤ f (Compr.toFun ((c, m), n)) ∧ (x ∈ A → Compr.toFun ((c, m), n) ∈ A)) : ∃ (g : PolyTimeFun Prog BitStr), ∀ (e : Prog), (Halts e Data.nil → g.toFun e ∈ A) ∧ (¬Halts e Data.nil → f (g.toFun e) = ⊤)

Recursive compression lemma ([MNY, Lemma 5.1]; blueprint lem:recursive-compression).

Data: f : {0,1}* → ℕ∞, a nonempty language A on which f is finite, and a polynomial-time compression procedure Compr taking a (claimed) succinct description (c, m) and a target parameter n, such that whenever (c, m) genuinely describes x:

1. f (Compr ((c, m), n)) ≥ max (f x) n, and
2. x ∈ A → Compr ((c, m), n) ∈ A.

Conclusion: a polynomial-time reduction g from the halting problem (of the ambient model, on the empty input nil) to A, with f (g e) = ∞ on non-halting e.

There are no computability assumptions on f, and no assumptions on the output of Compr off succinct descriptions (but Compr is total and fast everywhere — [MNY, §7] shows this is essential). The finiteness hypothesis hA is part of the statement of [MNY] (it makes the two conclusions exclusive) but is not needed for the proof.

Lin's compressibility criterion

The value-form abstract lemma (blueprint lem:compressible-criterion): Lin's compression criterion for RE-complete problems ([Lin, MIP^co = coRE, "Compression criteria for RE-complete problems", direction (3) ⇒ (1)]), in the succinct-description formulation of [MNY]. Compared with recursive_compression, the growth hypothesis on a measure f is replaced by a second preserved class B whose complement is semidecidable, and the self-referential decider gains a search branch: at level n it also runs, for Nat.size n steps, the semidecision procedure on the string at the start of the recursion. The start level m is carried as data next to the level n (the decider's input is (c', (e, (m, n)))), so that the decider's code does not depend on the threshold, which is chosen afterwards from the decider's time bound exactly as in recursive_compression.

The lemma is proved in a per-level form (compressibility_criterion_levels): the classes A n, B n are indexed by the level, the semidecider runs on (x, n), and the compression hypothesis is only required of short descriptions with parameter the level, transferring the class at level 2n + 1 to the class at level n — precisely what the proof uses. The level-free statement (compressibility_criterion) is its special case.

def MIPRE.Cost.levels (R : ℕ) : ℕ → ℕ

The levels of the recursion started at R: R, 2R + 1, 4R + 3, ….

Equations

• MIPRE.Cost.levels R 0 = R
• MIPRE.Cost.levels R k.succ = 2 * MIPRE.Cost.levels R k + 1

@[simp]

theorem MIPRE.Cost.levels_zero (R : ℕ) : levels R 0 = R

@[simp]

theorem MIPRE.Cost.levels_succ (R k : ℕ) : levels R (k + 1) = 2 * levels R k + 1

theorem MIPRE.Cost.le_levels (R k : ℕ) : R ≤ levels R k

theorem MIPRE.Cost.levels_mono (R : ℕ) {j k : ℕ} (h : j ≤ k) : levels R j ≤ levels R k

theorem MIPRE.Cost.two_pow_le_levels {R : ℕ} (hR : 1 ≤ R) (k : ℕ) : 2 ^ k ≤ levels R k

def MIPRE.Cost.Prog.searchProg (univ S : Prog) : Prog

The program of the search branch. On the pair (d, input) with d = encode ((c', (e, (m, m))), m) (the input is ignored), run univ on the first component of d — that is, c' on encode (e, (m, m)), the string at the start level m — and then S on the pair of the result with the start level m. Hardcoding d (hardcode (searchProg univ S) d) gives the program the search branch tests for halting.

Equations

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

theorem MIPRE.Cost.Prog.searchProg_wellScoped {univ S : Prog} (hU : WellScoped 1 univ) (hS : WellScoped 1 S) : WellScoped 1 (univ.searchProg S)

theorem MIPRE.Cost.Prog.searchProg_runs (U : UniversalMachine) {S : Prog} (hS : WellScoped 1 S) {c' e : Prog} {m : ℕ} {x r : Data} {tx ts : ℕ} (hx : c'.Runs (encode (e, m, m)) x tx) (hSr : S.Runs (x.cons (encode m)) r ts) : ∃ (T : ℕ), (hardcode (U.univ.searchProg S) (encode ((c', e, m, m), m))).Runs Data.nil r T

Forward: if c' on encode (e, (m, m)) produces x and S halts on (x, m), then the hardcoded search program halts on the empty input.

theorem MIPRE.Cost.Prog.searchProg_halts_of (U : UniversalMachine) {S : Prog} (hS : WellScoped 1 S) {c' e : Prog} {m : ℕ} {r : Data} {T : ℕ} (h : (hardcode (U.univ.searchProg S) (encode ((c', e, m, m), m))).Runs Data.nil r T) : ∃ (x : Data) (tx : ℕ), c'.Runs (encode (e, m, m)) x tx ∧ Halts S (x.cons (encode m))

Backward: a run of the hardcoded search program on the empty input yields a run of c' on encode (e, (m, m)) to some x such that S halts on (x, m).

noncomputable def MIPRE.Cost.decFunV (U : UniversalMachine) (UT : ClockedUniversalMachine) (S : Prog) (Compr : PolyTimeFun (Prog × ℕ) BitStr) (yYes yNo : BitStr) : PolyTimeFun (Prog × Prog × ℕ × ℕ) BitStr

The decider of the compressibility-criterion argument, as a polynomial-time function of (c', (e, (m, n))): if e halts on the empty input within Nat.size n steps, the fixed string yYes; else if the search program for the string at the start level m halts within Nat.size n steps, the fixed string yNo; otherwise Compr applied to the succinct description hardcode β ((c', e), (m, 2n + 1)) — where β is the bit-query program — with parameter n. As for decFun, the self-referential program c of the proof is a Kleene fixed point of c' ↦ hardcode (decFunV …).code (encode c').

Equations

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

theorem MIPRE.Cost.decFunV_apply (U : UniversalMachine) (UT : ClockedUniversalMachine) (S : Prog) (Compr : PolyTimeFun (Prog × ℕ) BitStr) (yYes yNo : BitStr) (c' e : Prog) (m n : ℕ) : (decFunV U UT S Compr yYes yNo).toFun (c', e, m, n) = if (evalWithin e Data.nil n.size).isSome = true then yYes else if (evalWithin (hardcode (U.univ.searchProg S) (encode ((c', e, m, m), m))) Data.nil n.size).isSome = true then yNo else Compr.toFun (hardcode U.univ.bitQueryProg (encode ((c', e), m, 2 * n + 1)), n)

theorem MIPRE.Cost.compressibility_criterion_nested (A B₀ B₁ : ℕ → Set BitStr) (n₀ : ℕ) (hsub : ∀ (n : ℕ), B₀ n ⊆ B₁ n) (yYes : BitStr) (hyes : ∀ (n : ℕ), n₀ ≤ n → yYes ∈ A n) (yNo : BitStr) (hno : ∀ (n : ℕ), n₀ ≤ n → yNo ∈ B₀ n) (S : Prog) (hSws : Prog.WellScoped 1 S) (hS : ∀ (x : BitStr) (n : ℕ), Halts S (encode (x, n)) ↔ x ∉ B₁ n) (Compr : PolyTimeFun (Prog × ℕ) BitStr) (hCompr : ∀ (c : Prog) (x : BitStr) (n : ℕ), n₀ ≤ n → 2 * esize c ≤ n → IsSuccinctDesc c n x → List.length x ≤ n + 1 → (x ∈ A (2 * n + 1) → Compr.toFun (c, n) ∈ A n) ∧ (x ∈ B₀ (2 * n + 1) → Compr.toFun (c, n) ∈ B₀ n)) : ∃ (g : PolyTimeFun Prog BitStr) (K : ℕ), ∀ (e : Prog), n₀ ≤ 2 ^ (K + 1 + esize e) ∧ (Halts e Data.nil → g.toFun e ∈ A (2 ^ (K + 1 + esize e))) ∧ (¬Halts e Data.nil → g.toFun e ∈ B₁ (2 ^ (K + 1 + esize e)))

Compressibility criterion, per level, with nested classes (blueprint lem:compressible-criterion-nested): compressibility_criterion_levels with the class B split in two, B₀ n ⊆ B₁ n. The distinguished string yNo lies in the smaller class and the compressor preserves it, while the semidecision procedure S recognizes the complement of the larger one; the conclusion for a non-halting e is membership in the larger class.

This is the form the coRE direction of MIP^co = coRE needs (planning/mipco-track.md §3): there A is the class of small commuting-operator value, B₀ the class of the main theorem — a perfect PCC strategy, preserved by the tensor completeness of compression — and B₁ the class of commuting-operator value 1, whose complement the upper semidecider for that value recognizes and which no compression theorem preserves. The proof is that of compressibility_criterion_levels unchanged: the downward induction that puts every level of the recursion in B runs inside B₀ from yNo, and a firing search contradicts membership in B₀ through B₀ ⊆ B₁.

theorem MIPRE.Cost.compressibility_criterion_levels (A B : ℕ → Set BitStr) (n₀ : ℕ) (yYes : BitStr) (hyes : ∀ (n : ℕ), n₀ ≤ n → yYes ∈ A n) (yNo : BitStr) (hno : ∀ (n : ℕ), n₀ ≤ n → yNo ∈ B n) (S : Prog) (hSws : Prog.WellScoped 1 S) (hS : ∀ (x : BitStr) (n : ℕ), Halts S (encode (x, n)) ↔ x ∉ B n) (Compr : PolyTimeFun (Prog × ℕ) BitStr) (hCompr : ∀ (c : Prog) (x : BitStr) (n : ℕ), n₀ ≤ n → 2 * esize c ≤ n → IsSuccinctDesc c n x → List.length x ≤ n + 1 → (x ∈ A (2 * n + 1) → Compr.toFun (c, n) ∈ A n) ∧ (x ∈ B (2 * n + 1) → Compr.toFun (c, n) ∈ B n)) : ∃ (g : PolyTimeFun Prog BitStr) (K : ℕ), ∀ (e : Prog), n₀ ≤ 2 ^ (K + 1 + esize e) ∧ (Halts e Data.nil → g.toFun e ∈ A (2 ^ (K + 1 + esize e))) ∧ (¬Halts e Data.nil → g.toFun e ∈ B (2 ^ (K + 1 + esize e)))

Compressibility criterion, per level (Lin; blueprint lem:compressible-criterion), the value-form abstract compression lemma in the form an instantiation by gap-preserving compression can meet. The case B₀ = B₁ = B of compressibility_criterion_nested, which is where the proof is.

Data: two families of languages A n, B n indexed by the level n of the recursion, with distinguished elements yYes ∈ A n and yNo ∈ B n at every level n ≥ n₀; a semidecision procedure S for the complement of B (a closed program halting on encode (x, n) exactly when x ∉ B n); and a polynomial-time compression procedure Compr taking a (claimed) succinct description c with parameter n — the level — such that whenever n ≥ n₀, c is short (2 · |c| ≤ n) and genuinely describes x with parameter n:

1. x ∈ A (2n + 1) → Compr (c, n) ∈ A n, and
2. x ∈ B (2n + 1) → Compr (c, n) ∈ B n.

Conclusion: a polynomial-time reduction g from the halting problem (of the ambient model, on the empty input nil) and a constant K such that, with R e = 2 ^ (K + 1 + |e|) (a level at least n₀), g e ∈ A (R e) on halting e and g e ∈ B (R e) on non-halting e.

The level bookkeeping is what an instantiation needs. The compressor is polynomial-time in the size of its input (c, n), that is, polylogarithmic in n, while a bit query to c costs up to n — so Compr cannot read the string x it is compressing, only embed c into its output for a later reader (a decider at index n, whose time budget is polynomial in n); the slack 2 · |c| ≤ n is what lets that output stay short. And the hypothesis relates the class of x at level 2n + 1 to the class of the output at level n, which is exactly what the proof uses: at level n the self-referential decider compresses the string it itself computes at level 2n + 1. See the module docstring for the reading of the levels in the instantiation. Nothing is demanded of Compr off short genuine descriptions above n₀, but it is total and fast everywhere.

There is no measure and no growth hypothesis: the self-referential decider at level n compresses the next level 2n + 1, unless e halts within Nat.size n steps (output yYes) or the semidecision procedure, run on the string at the start level of the recursion, halts within Nat.size n steps (output yNo). Non-halting e: if the start string were outside B, the search branch would eventually fire, and preservation of B down the levels would put the start string in B. Halting e: the search branch can never fire before e halts, by the same downward argument, so preservation of A down from the level where e halts applies.

theorem MIPRE.Cost.compressibility_criterion (A B : Set BitStr) (yYes : BitStr) (hyes : yYes ∈ A) (yNo : BitStr) (hno : yNo ∈ B) (S : Prog) (hSws : Prog.WellScoped 1 S) (hS : ∀ (x : BitStr), Halts S (encode x) ↔ x ∉ B) (Compr : PolyTimeFun ((Prog × ℕ) × ℕ) BitStr) (hCompr : ∀ (c : Prog) (m : ℕ) (x : BitStr) (n : ℕ), IsSuccinctDesc c m x → (x ∈ A → Compr.toFun ((c, m), n) ∈ A) ∧ (x ∈ B → Compr.toFun ((c, m), n) ∈ B)) : ∃ (g : PolyTimeFun Prog BitStr), ∀ (e : Prog), (Halts e Data.nil → g.toFun e ∈ A) ∧ (¬Halts e Data.nil → g.toFun e ∈ B)

Compressibility criterion (Lin; blueprint lem:compressible-criterion), the value-form abstract compression lemma in its level-free form: the special case of compressibility_criterion_levels with the same classes at every level and a compressor that receives the parameter of the succinct description separately from the level.

Data: two languages A, B with distinguished elements yYes ∈ A and yNo ∈ B; a semidecision procedure S for the complement of B (a closed program halting on encode x exactly when x ∉ B); and a polynomial-time compression procedure Compr taking a (claimed) succinct description (c, m) and a target parameter n, such that whenever (c, m) genuinely describes x:

1. x ∈ A → Compr ((c, m), n) ∈ A, and
2. x ∈ B → Compr ((c, m), n) ∈ B.

Conclusion: a polynomial-time reduction g from the halting problem (of the ambient model, on the empty input nil) with g e ∈ A on halting e and g e ∈ B on non-halting e. This is the form of [Lin], [MNY]; the per-level form is the one the instantiation by gap-preserving compression can satisfy (blueprint rem:compression-abstract).

Interface with Mathlib computability

The project's headline statement (MIPRE.HaltingGameValue) is phrased for Nat.Partrec.Code and Mathlib's Computable. Two bridges close the gap, both computability-only (no time bounds): ambient evaluation is partial recursive, so a polynomial-time function of the model is Mathlib-computable on computably encoded inputs (PolyTimeFun.computable_comp, Cost/Partrec.lean), and the halting problem of Nat.Partrec.Code compiles into the model along a map that is computable on descriptions (exists_compile, Cost/FromPartrec.lean). Both work at the level of Data: no Primcodable instance for Prog is needed, since programs are their own descriptions.

theorem MIPRE.Cost.recursive_compression_halting (f : BitStr → ℕ∞) (A : Set BitStr) (y₀ : BitStr) (hy₀ : y₀ ∈ A) (hA : ∀ x ∈ A, f x < ⊤) (Compr : PolyTimeFun ((Prog × ℕ) × ℕ) BitStr) (hCompr : ∀ (c : Prog) (m : ℕ) (x : BitStr) (n : ℕ), IsSuccinctDesc c m x → max (f x) ↑n ≤ f (Compr.toFun ((c, m), n)) ∧ (x ∈ A → Compr.toFun ((c, m), n) ∈ A)) : ∃ (g : Nat.Partrec.Code → BitStr), Computable g ∧ ∀ (pc : Nat.Partrec.Code), ((pc.eval 0).Dom → g pc ∈ A) ∧ (¬(pc.eval 0).Dom → f (g pc) = ⊤)

The compression lemma, repackaged against Mathlib's halting problem, in the abstract form of rem:compression-abstract: A and f stand for normal-form-verifier games and the entanglement requirement (blueprint thm:halting). The headline HaltingGameValue.halting_reduces_to_gameValue is proved through GapCompression instead (MIPRE/MainTheorem.lean).

theorem MIPRE.Cost.compressibility_criterion_halting (A B : Set BitStr) (yYes : BitStr) (hyes : yYes ∈ A) (yNo : BitStr) (hno : yNo ∈ B) (S : Prog) (hSws : Prog.WellScoped 1 S) (hS : ∀ (x : BitStr), Halts S (encode x) ↔ x ∉ B) (Compr : PolyTimeFun ((Prog × ℕ) × ℕ) BitStr) (hCompr : ∀ (c : Prog) (m : ℕ) (x : BitStr) (n : ℕ), IsSuccinctDesc c m x → (x ∈ A → Compr.toFun ((c, m), n) ∈ A) ∧ (x ∈ B → Compr.toFun ((c, m), n) ∈ B)) : ∃ (g : Nat.Partrec.Code → BitStr), Computable g ∧ ∀ (pc : Nat.Partrec.Code), ((pc.eval 0).Dom → g pc ∈ A) ∧ (¬(pc.eval 0).Dom → g pc ∈ B)

The compressibility criterion, repackaged against Mathlib's halting problem, in the abstract form of rem:compression-abstract: A and B stand for normal-form-verifier games having a perfect PCC strategy, respectively value at most 1/2 (blueprint thm:halting). The headline HaltingGameValue.halting_reduces_to_gameValue is proved through GapCompression instead (MIPRE/MainTheorem.lean).