The compressor's output is bounded: the accounting

Obligation O4, the accounting half: the verifier the compressor's output denotes is n-bounded at every level n past a threshold depending on G and U alone — the field CompressorSpec.isBounded_compr — and the parameter λ(n) it carries satisfies the growth conditions lam_ge and ansBound_le.

The parameter is λ(n) = 2 ^ (2 · size n), a 1 followed by zeros, so that the compressor can write it in binary in time polynomial in log n; it is at least (n + 1) ^ 2, which is what freezing the described verifier at index 2n + 1 needs (Verifier.freeze_isBounded through CompressorSpec.lam_ge).

Verifier.IsBounded n has three clauses at every index m ≥ 2 and a size clause, and each is absorbed by PolyBounded.absorb or PolyBounded.absorb_log (Halting/Absorb.lean) once the cost is written as a polynomially bounded function of the largest of the index, the level and the input size:

• the sampler is G.sampler (λ(n)), whose dimension and running time at index m are G.bound (m + λ(n)) (GapCompression.sampler_dim, sampler_time);
• the decider is the wrapper around haltProg with (c, n, λ(n)) hardcoded, whose cost on an input d is Prog.wrapCoreCost (Halting/WrapperCost.lean) with the inner cost innerBound: the preparation (prepBound), the universal machine on the compressed decider, and the compressed decider's own time G.bound (m + λ(n)) · (|d| + 1) ^ G.deg (GapCompression.decider_time);
• the size is that of the compressed sampler's program, polynomial in log n, and of the wrapper's description, which carries c — the slack 2|c| ≤ n of the criterion is what leaves room for it.

The parameter

def MIPRE.Halting.lamOf (n : ℕ) : ℕ

The parameter the output carries at level n: 2 ^ (2 · size n).

Equations

• MIPRE.Halting.lamOf n = 2 ^ (2 * n.size)

theorem MIPRE.Halting.polyBounded_lamOf : Cost.PolyBounded lamOf

theorem MIPRE.Halting.size_lamOf (n : ℕ) : (lamOf n).size = 2 * n.size + 1

theorem MIPRE.Halting.esize_lamOf_le (n : ℕ) : Cost.esize (lamOf n) ≤ 8 * n.size + 5

theorem MIPRE.Halting.sq_le_lamOf (n : ℕ) : (n + 1) ^ 2 ≤ lamOf n

λ(n) ≥ (n + 1) ^ 2.

theorem MIPRE.Halting.lamOf_mono {n n' : ℕ} (h : n ≤ n') : lamOf n ≤ lamOf n'

λ(n) is monotone.

The output's verifier

def MIPRE.Halting.outDec (G : GapCompression) (U : Cost.UniversalMachine) (c : Cost.Prog) (n lam : ℕ) : Cost.Prog

The decider program the output carries: haltProg with (c, n, λ) hardcoded.

Equations

• MIPRE.Halting.outDec G U c n lam = MIPRE.Cost.hardcode (MIPRE.Halting.haltProg G U) (MIPRE.Cost.encode (c, n, lam))

theorem MIPRE.Halting.esize_outDec (G : GapCompression) (U : Cost.UniversalMachine) (c : Cost.Prog) (n lam : ℕ) : Cost.esize (outDec G U c n lam) = Cost.esize (haltProg G U) + Cost.esize c + Cost.esize n + Cost.esize lam + 37

theorem MIPRE.Halting.Vof_comprStr' (G : GapCompression) (U : Cost.UniversalMachine) (c : Cost.Prog) (n lam : ℕ) : Vof G U (comprStr G U c n lam) = Verifier.ofSamplerDecider U (G.sampler lam) (outDec G U c n lam)

The sampler clauses

noncomputable def MIPRE.Halting.sampZ (G : GapCompression) (z : ℕ) : ℕ

The dimension and running-time bound of the compressed sampler at λ(n), index m, as a polynomially bounded function of the largest of m and n.

Equations

• MIPRE.Halting.sampZ G z = Polynomial.eval (z + MIPRE.Halting.lamOf z) G.bound

theorem MIPRE.Halting.polyBounded_sampZ (G : GapCompression) : Cost.PolyBounded (sampZ G)

theorem MIPRE.Halting.bound_le_sampZ (G : GapCompression) {m n z : ℕ} (hm : m ≤ z) (hn : n ≤ z) : Polynomial.eval (m + lamOf n) G.bound ≤ sampZ G z

theorem MIPRE.Halting.sampler_clauses (G : GapCompression) : ∃ (n₀ : ℕ), ∀ (n : ℕ), n₀ ≤ n → ∀ (m : ℕ), 2 ≤ m → (G.sampler (lamOf n)).dim m ≤ m ^ n ∧ (G.sampler (lamOf n)).TimeBoundAt m (m ^ n) n

The sampler clauses: past a threshold, at every index m ≥ 2 the compressed sampler at λ(n) has dimension at most m ^ n and runs within m ^ n · (|d| + 1) ^ n.

The size clause

noncomputable def MIPRE.Halting.sizeZ (G : GapCompression) (U : Cost.UniversalMachine) (s : ℕ) : ℕ

The size of the output's verifier, beyond the description c it carries, as a function of size n.

Equations

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

theorem MIPRE.Halting.polyBounded_sizeZ (G : GapCompression) (U : Cost.UniversalMachine) : Cost.PolyBounded (sizeZ G U)

theorem MIPRE.Halting.esize_sampler_le (G : GapCompression) (n : ℕ) : Cost.esize (G.sampler (lamOf n)).prog ≤ Polynomial.eval (8 * n.size + 5) G.samplerProg.timeBound

The compressed sampler's program at λ(n) has size polynomial in size n.

theorem MIPRE.Halting.esize_wrapCore_le (G : GapCompression) (U : Cost.UniversalMachine) (c : Cost.Prog) (n : ℕ) : Cost.esize (U.univ.wrapCore (G.sampler (lamOf n)).prog (Cost.encode (outDec G U c n (lamOf n)))) ≤ Cost.esize c + sizeZ G U n.size

The output's decider — the wrapper around outDec — has size at most |c| + sizeZ (size n).

theorem MIPRE.Halting.size_clause (G : GapCompression) (U : Cost.UniversalMachine) : ∃ (n₀ : ℕ), ∀ (n : ℕ), n₀ ≤ n → ∀ (c : Cost.Prog), 2 * Cost.esize c ≤ n → (Vof G U (comprStr G U c n (lamOf n))).size ≤ n

The size clause: past a threshold, a description of size at most n / 2 yields an output whose verifier has size at most n.

The decider clause

The output's decider is the wrapper around outDec; its cost on an input d at index m is Prog.wrapCoreCost with the inner cost innerBound below. Both are then bounded by a polynomially bounded function decZ of the largest of the index m, the level n and the input size |d|, and absorbed.

noncomputable def MIPRE.Halting.innerBound (G : GapCompression) (U : Cost.UniversalMachine) (s n L lam l m t : ℕ) : ℕ

The inner decider's cost at index m on an input of size t: for a description of size s of a string of length L, at level n and parameter lam of size l. The sizes of the binary numerals m and n appear as 4 · size + 1, so that the bound is monotone.

Equations

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

theorem MIPRE.Halting.outDec_cost (G : GapCompression) (U : Cost.UniversalMachine) {c : Cost.Prog} {x : Cost.BitStr} {n : ℕ} (hsd : Cost.IsSuccinctDesc c n x) (lam m : ℕ) (d : Cost.Data) : ∃ (r : Cost.Data), ∃ t ≤ innerBound G U (Cost.esize c) n (List.length x) lam (Cost.esize lam) m d.size, (outDec G U c n lam).Runs ((Cost.encode m).cons d) r t

The inner decider's cost. On a succinct description (c, n) of x, outDec with (c, n, λ) runs within innerBound on every input at every index: the compressed decider's own time (GapCompression.decider_time), simulated by the universal machine, after the preparation.

theorem MIPRE.Halting.outDec_wrap_cost (G : GapCompression) (U : Cost.UniversalMachine) {c : Cost.Prog} {x : Cost.BitStr} {n : ℕ} (hsd : Cost.IsSuccinctDesc c n x) (m : ℕ) (d : Cost.Data) : ∃ (r : Cost.Data), ∃ t ≤ Cost.Prog.wrapCoreCost U (G.sampler (lamOf n)) (outDec G U c n (lamOf n)) (fun (m : ℕ) => Polynomial.eval (m + lamOf n) G.bound) G.deg m (innerBound G U (Cost.esize c) n (List.length x) (lamOf n) (Cost.esize (lamOf n)) m d.size) d.size, (U.univ.wrapCore (G.sampler (lamOf n)).prog (Cost.encode (outDec G U c n (lamOf n)))).Runs ((Cost.encode m).cons d) r t

The output's decider, on every input.

Monotonicity and polynomial boundedness of the bounds

theorem MIPRE.Halting.readIter_mono (U : Cost.UniversalMachine) {s s' n n' L L' : ℕ} (hs : s ≤ s') (hn : n ≤ n') (hL : L ≤ L') : Cost.Prog.readIter U s n L ≤ Cost.Prog.readIter U s' n' L'

theorem MIPRE.Halting.sampBound_mono (G : GapCompression) {L L' : ℕ} (hL : L ≤ L') : sampBound G L ≤ sampBound G L'

theorem MIPRE.Halting.wBound_mono (G : GapCompression) (U : Cost.UniversalMachine) {L L' : ℕ} (hL : L ≤ L') : wBound G U L ≤ wBound G U L'

theorem MIPRE.Halting.kBound_mono {n n' : ℕ} (hn : n ≤ n') : kBound n ≤ kBound n'

theorem MIPRE.Halting.fBound_mono (G : GapCompression) (U : Cost.UniversalMachine) {L L' n n' : ℕ} (hL : L ≤ L') (hn : n ≤ n') : fBound G U L n ≤ fBound G U L' n'

theorem MIPRE.Halting.prepBound_mono (G : GapCompression) (U : Cost.UniversalMachine) {s s' n n' L L' l l' : ℕ} (hs : s ≤ s') (hn : n ≤ n') (hL : L ≤ L') (hl : l ≤ l') : prepBound G U s n L l ≤ prepBound G U s' n' L' l'

theorem MIPRE.Halting.innerBound_mono (G : GapCompression) (U : Cost.UniversalMachine) {s s' n n' L L' lam lam' l l' m m' t t' : ℕ} (hs : s ≤ s') (hn : n ≤ n') (hL : L ≤ L') (hlam : lam ≤ lam') (hl : l ≤ l') (hm : m ≤ m') (ht : t ≤ t') : innerBound G U s n L lam l m t ≤ innerBound G U s' n' L' lam' l' m' t'

PolyBounded for each bound, with every argument the same z.

theorem MIPRE.Halting.polyBounded_readIter (U : Cost.UniversalMachine) : Cost.PolyBounded fun (z : ℕ) => Cost.Prog.readIter U z z (z + 1)

theorem MIPRE.Halting.polyBounded_sampBound (G : GapCompression) : Cost.PolyBounded fun (z : ℕ) => sampBound G (z + 1)

theorem MIPRE.Halting.polyBounded_wBound (G : GapCompression) (U : Cost.UniversalMachine) : Cost.PolyBounded fun (z : ℕ) => wBound G U (z + 1)

theorem MIPRE.Halting.polyBounded_kBound : Cost.PolyBounded kBound

theorem MIPRE.Halting.polyBounded_fBound (G : GapCompression) (U : Cost.UniversalMachine) : Cost.PolyBounded fun (z : ℕ) => fBound G U (z + 1) z

theorem MIPRE.Halting.polyBounded_lsize : Cost.PolyBounded fun (z : ℕ) => 8 * z.size + 5

The size of λ(z)'s encoding, as the bound 8 · size z + 5.

theorem MIPRE.Halting.polyBounded_prepBound (G : GapCompression) (U : Cost.UniversalMachine) : Cost.PolyBounded fun (z : ℕ) => prepBound G U z z (z + 1) (8 * z.size + 5)

theorem MIPRE.Halting.polyBounded_innerBound (G : GapCompression) (U : Cost.UniversalMachine) : Cost.PolyBounded fun (z : ℕ) => innerBound G U z z (z + 1) (lamOf z) (8 * z.size + 5) z z

The master bound, and the clause

noncomputable def MIPRE.Halting.sigZ (G : GapCompression) (z : ℕ) : ℕ

The size of the compressed sampler's program, in z.

Equations

• MIPRE.Halting.sigZ G z = Polynomial.eval (8 * z.size + 5) G.samplerProg.timeBound

def MIPRE.Halting.deltaZ (G : GapCompression) (U : Cost.UniversalMachine) (z : ℕ) : ℕ

The size of the output's inner decider outDec, in z.

Equations

• MIPRE.Halting.deltaZ G U z = MIPRE.Cost.esize (MIPRE.Halting.haltProg G U) + z + (4 * z.size + 1) + (8 * z.size + 5) + 37

noncomputable def MIPRE.Halting.iotaZ (G : GapCompression) (U : Cost.UniversalMachine) (z : ℕ) : ℕ

The inner cost, in z.

Equations

• MIPRE.Halting.iotaZ G U z = MIPRE.Halting.innerBound G U z z (z + 1) (MIPRE.Halting.lamOf z) (8 * z.size + 5) z z

noncomputable def MIPRE.Halting.headZ (G : GapCompression) (U : Cost.UniversalMachine) (z : ℕ) : ℕ

wrapHeadZ, in z.

Equations

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

noncomputable def MIPRE.Halting.decZ (G : GapCompression) (U : Cost.UniversalMachine) (z : ℕ) : ℕ

The master bound: wrapCoreCost with every atom replaced by its bound in z.

Equations

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

theorem MIPRE.Halting.polyBounded_sigZ (G : GapCompression) : Cost.PolyBounded (sigZ G)

theorem MIPRE.Halting.polyBounded_deltaZ (G : GapCompression) (U : Cost.UniversalMachine) : Cost.PolyBounded (deltaZ G U)

theorem MIPRE.Halting.polyBounded_iotaZ (G : GapCompression) (U : Cost.UniversalMachine) : Cost.PolyBounded (iotaZ G U)

theorem MIPRE.Halting.polyBounded_headZ (G : GapCompression) (U : Cost.UniversalMachine) : Cost.PolyBounded (headZ G U)

theorem MIPRE.Halting.polyBounded_decZ (G : GapCompression) (U : Cost.UniversalMachine) : Cost.PolyBounded (decZ G U)

theorem MIPRE.Halting.wrapCoreCost_le_decZ (G : GapCompression) (U : Cost.UniversalMachine) {c : Cost.Prog} {x : Cost.BitStr} {n m t z : ℕ} (hc : Cost.esize c ≤ n) (hx : List.length x ≤ n + 1) (hm : m ≤ z) (hn : n ≤ z) (ht : t ≤ z) : Cost.Prog.wrapCoreCost U (G.sampler (lamOf n)) (outDec G U c n (lamOf n)) (fun (m : ℕ) => Polynomial.eval (m + lamOf n) G.bound) G.deg m (innerBound G U (Cost.esize c) n (List.length x) (lamOf n) (Cost.esize (lamOf n)) m t) t ≤ decZ G U z

The output's decider cost is below the master bound at the largest z of the index, the level and the input size.

theorem MIPRE.Halting.decider_clause (G : GapCompression) (U : Cost.UniversalMachine) : ∃ (n₀ : ℕ), ∀ (n : ℕ), n₀ ≤ n → ∀ (c : Cost.Prog) (x : Cost.BitStr), 2 * Cost.esize c ≤ n → Cost.IsSuccinctDesc c n x → List.length x ≤ n + 1 → ∀ (m : ℕ), 2 ≤ m → (Vof G U (comprStr G U c n (lamOf n))).decider.TimeBoundAt m (m ^ n) n

The decider clause: past a threshold, on a succinct description (c, n) of a string of length at most n + 1 with 2|c| ≤ n, the output's decider runs within m ^ n · (|d| + 1) ^ n at every index m ≥ 2.

The output is bounded

theorem MIPRE.Halting.isBounded_comprStr (G : GapCompression) (U : Cost.UniversalMachine) : ∃ (n₀ : ℕ), ∀ (n : ℕ), n₀ ≤ n → ∀ (c : Cost.Prog) (x : Cost.BitStr), 2 * Cost.esize c ≤ n → Cost.IsSuccinctDesc c n x → List.length x ≤ n + 1 → (Vof G U (comprStr G U c n (lamOf n))).IsBounded n

The field isBounded_compr.

The growth of the parameter

theorem MIPRE.Halting.size_two_mul_add_one_le (n : ℕ) : (2 * n + 1).size ≤ n.size + 1

size (2n + 1) ≤ size n + 1.

theorem MIPRE.Halting.lamOf_ge : ∃ (n₀ : ℕ), ∀ (n : ℕ), n₀ ≤ n → (2 * n + 1) ^ (2 * n + 1) + Cost.esize (2 * n + 1) + 4 ≤ 2 ^ lamOf n ∧ 2 * n + 1 + Cost.esize (2 * n + 1) + 53 ≤ lamOf n

The field lam_ge: the growth Verifier.freeze_isBounded needs of λ(n).

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

The field ansBound_le, from exists_ansBound_le at λ(n) ≥ n + 1.

The specification, given the compressor's program

theorem MIPRE.Halting.exists_compressorSpec (G : GapCompression) (U : Cost.UniversalMachine) (compr : Cost.PolyTimeFun (Cost.Prog × ℕ) Cost.BitStr) (hcompr : ∀ (c : Cost.Prog) (n : ℕ), compr.toFun (c, n) = comprStr G U c n (lamOf n)) : ∃ (S : CompressorSpec G U), S.compr = compr ∧ S.lam = lamOf

The compressor meets its specification, given a polynomial-time program computing comprStr c n (λ(n)) from (c, n). Everything the specification asks is proved here or in Halting/Compressor.lean; the program itself is the last piece of obligation O4.