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): A = descriptions of normal form verifier games with a perfect PCC strategy, B = descriptions of games with value at most 1/2, and S = the enumeration of strategies of value above 1/2 (blueprint lem:value-lower-approx), composed with the interpretation of descriptions as games. 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.

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))) (the input is ignored), run univ on d — that is, c' on encode (e, (m, m)), the string at the start level m — and then S on the result. Hardcoding d (hardcode (searchProg univ S) d) gives the program the search branch tests for halting.

Equations

• univ.searchProg S = MIPRE.Cost.Prog.elim 0 MIPRE.Cost.Prog.nil ((MIPRE.Cost.Prog.callVar 0 univ).let_ (MIPRE.Cost.Prog.callVar 0 S))

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 r ts) : ∃ (T : ℕ), (hardcode (U.univ.searchProg S) (encode (c', e, m, m))).Runs Data.nil r T

Forward: if c' on encode (e, (m, m)) produces x and S halts on x, 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))).Runs Data.nil r T) : ∃ (x : Data) (tx : ℕ), c'.Runs (encode (e, m, m)) x tx ∧ Halts S x

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 on which S halts.

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)), n) — 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))) Data.nil n.size).isSome = true then yNo else Compr.toFun ((hardcode U.univ.bitQueryProg (encode ((c', e), m, 2 * n + 1)), n), n)

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.

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. 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.

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 — the form that will feed MIPRE.HaltingGameValue.halting_reduces_to_gameValue once A and f are instantiated with normal-form-verifier games and the entanglement requirement (blueprint rem:compression-abstract and thm:halting).

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 — the form that feeds MIPRE.HaltingGameValue.halting_reduces_to_gameValue once A and B are instantiated with normal-form-verifier games having a perfect PCC strategy, respectively value at most 1/2 (blueprint rem:compression-abstract and thm:halting).