The halting verifier along the paper's route: the accounting

Blueprint lem:lambda in the paper's form (recursive.tex), for the polynomial-time halting reduction of planning/polytime-halting.md: the verifier Vhalt M λ is λ-bounded (Verifier.IsBounded λ) as soon as λ ≥ Λ₀ + 4|M|, for a threshold Λ₀ depending on the compressor, the universal machines and the search program alone — and at such λ the compressor's bound poly(n, λ) is below n ^ λ at every level n ≥ 2, which is what the induction of Paper/Induction.lean runs on.

The accounting has three layers.

• The decider's run (dec_cost): on (n, d), dec M λ runs within decRunZ z |d| at z = n + |M| + λ, an explicit expression assembled along the fixed point's time transfer (Cost.kleeneFix_runs_of), the hardcoding of the description (hardcode_time), the run of prep (its timeBound), the universal machine on what prep returns (U.time_le) and the compressed decider's own time (GapCompression.decider_time). decRunZ is a PolyCost, so the run is within Q(n + |M| + λ) · (|d| + 1) ^ k for a polynomial Q and a degree k depending on G, U, UT, S' alone (decCostPoly, decCostDeg, dec_cost_spec). This fine form, polynomial in the level with |M| and λ as parameters, is what the class verifier of the paper's MIP* needs at the fixed level C; IsBounded only records n ^ λ.
• The wrapped decider (Vhalt_decider_cost): Prog.wrapCoreCost of Halting/WrapperCost with the inner cost above, bounded by the master expression WZ z at the largest z of the index, |M|, λ and the input size (wrapCoreCost_le_WZ).
• The clauses of IsBounded λ, each absorbed past a threshold by PolyBounded.absorb (the dimension, the sampler's and the decider's times, and the parameter inequality poly(n, λ) ≤ n ^ λ) or PolyBounded.absorb_log (the size, where the decider's description is 2 (|M| + |λ|) plus a constant, so that λ ≥ Λ₀ + 4|M| leaves room for it).

The threshold is existential (exists_lamBound, Lam0), as in lem:lambda: the paper's λ(M) = poly(|M|) is here the affine Λ₀ + 4|M|, and the constant Λ₀ is whatever the absorption thresholds are.

What prep returns

def MIPRE.Halting.constCost : ℕ

The cost of the two constant programs: the sizes of encode true and encode false.

Equations

• MIPRE.Halting.constCost = (MIPRE.Cost.encode true).size + (MIPRE.Cost.encode false).size

noncomputable def MIPRE.Halting.progSize (G : GapCompression) (U : Cost.UniversalMachine) (lam : ℕ) (e : Cost.Prog) : ℕ

The size of the program prep returns, at the parameter λ and the inner decider e: the compressed decider's, from compress's time bound at the size of its input.

Equations

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

theorem MIPRE.Halting.esize_wrapCore (U : Cost.UniversalMachine) (s e : Cost.Prog) : Cost.esize (U.univ.wrapCore s (Cost.encode e)) = Cost.esize s + Cost.esize e + 2 * Cost.esize U.univ + Cost.Prog.ProgD.wrapNodes

The description wrapCore univ s (encode e) has size |s| + |e| + 2|univ| + wrapNodes.

theorem MIPRE.Halting.prep_output (G : GapCompression) (U : Cost.UniversalMachine) (UT : Cost.ClockedUniversalMachine) (S' M : Cost.Prog) (lam : ℕ) (e : Cost.Prog) (n : ℕ) (d : Cost.Data) : Cost.esize ((prep G U UT S').toFun ((M, lam, e), n, d)).1 ≤ progSize G U lam e ∧ ((prep G U UT S').toFun ((M, lam, e), n, d)).2.size ≤ Cost.esize n + d.size + 1 ∧ ∃ (r : Cost.Data), ∃ t ≤ Polynomial.eval (n + lam) G.bound * (d.size + 1) ^ G.deg + constCost, ((prep G U UT S').toFun ((M, lam, e), n, d)).1.Runs ((prep G U UT S').toFun ((M, lam, e), n, d)).2 r t

What prep returns, on the description (M, (λ, e)) and the input (n, d): a program of size at most progSize λ e, an input of size at most |n| + |d| + 1, and the program runs on the input within the compressed decider's time plus a constant.

The decider's run

Every atom of the cost — |n|, |M| + |λ|, |λ|, n, λ — is at most 4z + 1 or z at z = n + |M| + λ; muZ is the common bound on the encodings' sizes.

def MIPRE.Halting.muZ (z : ℕ) : ℕ

The common bound 5z + 1 on |n|, |M| + |λ| and |λ|.

Equations

• MIPRE.Halting.muZ z = 5 * z + 1

noncomputable def MIPRE.Halting.eZ (G : GapCompression) (U : Cost.UniversalMachine) (UT : Cost.ClockedUniversalMachine) (S' : Cost.Prog) (z : ℕ) : ℕ

The size of the decider, in z.

Equations

• MIPRE.Halting.eZ G U UT S' z = 2 * MIPRE.Halting.muZ z + MIPRE.Halting.cD G U UT S'

noncomputable def MIPRE.Halting.pZ (G : GapCompression) (U : Cost.UniversalMachine) (UT : Cost.ClockedUniversalMachine) (S' : Cost.Prog) (z : ℕ) : ℕ

The size of the description (M, (λ, dec M λ)), in z.

Equations

• MIPRE.Halting.pZ G U UT S' z = 3 * MIPRE.Halting.muZ z + MIPRE.Halting.cD G U UT S' + 2

noncomputable def MIPRE.Halting.feZ (G : GapCompression) (U : Cost.UniversalMachine) (UT : Cost.ClockedUniversalMachine) (S' : Cost.Prog) (z : ℕ) : ℕ

The size of F (dec M λ), in z.

Equations

• MIPRE.Halting.feZ G U UT S' z = MIPRE.Cost.esize (MIPRE.Halting.body G U UT S') + MIPRE.Halting.pZ G U UT S' z + 35

def MIPRE.Halting.vZ (z s : ℕ) : ℕ

The size of the input (n, d), in z and |d|.

Equations

• MIPRE.Halting.vZ z s = MIPRE.Halting.muZ z + s + 1

noncomputable def MIPRE.Halting.tpZ (G : GapCompression) (U : Cost.UniversalMachine) (UT : Cost.ClockedUniversalMachine) (S' : Cost.Prog) (z s : ℕ) : ℕ

The time of prep, in z and |d|.

Equations

• MIPRE.Halting.tpZ G U UT S' z s = Polynomial.eval (MIPRE.Halting.pZ G U UT S' z + MIPRE.Halting.vZ z s + 1) (MIPRE.Halting.prep G U UT S').timeBound

noncomputable def MIPRE.Halting.sigmaZ (G : GapCompression) (U : Cost.UniversalMachine) (UT : Cost.ClockedUniversalMachine) (S' : Cost.Prog) (z : ℕ) : ℕ

The size of the program prep returns, in z.

Equations

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

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

The time of the program prep returns, in z and |d|.

Equations

• MIPRE.Halting.tcZ G z s = Polynomial.eval (2 * z) G.bound * (s + 1) ^ G.deg + MIPRE.Halting.constCost

noncomputable def MIPRE.Halting.tuZ (G : GapCompression) (U : Cost.UniversalMachine) (UT : Cost.ClockedUniversalMachine) (S' : Cost.Prog) (z s : ℕ) : ℕ

The time of the universal machine on it, in z and |d|.

Equations

• MIPRE.Halting.tuZ G U UT S' z s = Polynomial.eval (MIPRE.Halting.sigmaZ G U UT S' z + MIPRE.Halting.vZ z s + MIPRE.Halting.tcZ G z s) U.bound

noncomputable def MIPRE.Halting.tbZ (G : GapCompression) (U : Cost.UniversalMachine) (UT : Cost.ClockedUniversalMachine) (S' : Cost.Prog) (z s : ℕ) : ℕ

The time of body, in z and |d|.

Equations

• MIPRE.Halting.tbZ G U UT S' z s = MIPRE.Halting.tpZ G U UT S' z s + (MIPRE.Halting.sigmaZ G U UT S' z + MIPRE.Halting.vZ z s + 1 + 1 + MIPRE.Halting.tuZ G U UT S' z s + 1) + 1

noncomputable def MIPRE.Halting.tfZ (G : GapCompression) (U : Cost.UniversalMachine) (UT : Cost.ClockedUniversalMachine) (S' : Cost.Prog) (z s : ℕ) : ℕ

The time of F (dec M λ), in z and |d|.

Equations

• MIPRE.Halting.tfZ G U UT S' z s = MIPRE.Halting.tbZ G U UT S' z s + MIPRE.Halting.pZ G U UT S' z + MIPRE.Halting.vZ z s + 3

noncomputable def MIPRE.Halting.ovZ (G : GapCompression) (U : Cost.UniversalMachine) (UT : Cost.ClockedUniversalMachine) (S' : Cost.Prog) (z : ℕ) : ℕ

The overhead of the fixed point's transfer, in z.

Equations

• MIPRE.Halting.ovZ G U UT S' z = 21 * MIPRE.Halting.muZ z + MIPRE.Halting.cO G U UT S'

noncomputable def MIPRE.Halting.decRunZ (G : GapCompression) (U : Cost.UniversalMachine) (UT : Cost.ClockedUniversalMachine) (S' : Cost.Prog) (z s : ℕ) : ℕ

The master bound on the decider's run, in z and |d|.

Equations

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

theorem MIPRE.Halting.dec_cost (G : GapCompression) (U : Cost.UniversalMachine) (UT : Cost.ClockedUniversalMachine) (S' M : Cost.Prog) (lam n : ℕ) (d : Cost.Data) : ∃ (r : Cost.Data), ∃ t ≤ decRunZ G U UT S' (n + Cost.esize M + lam) d.size, (dec G U UT S' M lam).Runs ((Cost.encode n).cons d) r t

The decider's run: on (n, d), dec M λ halts within decRunZ (n + |M| + λ) |d|.

The polynomial form

theorem MIPRE.Halting.polyCost_pow_size (k : ℕ) : Cost.PolyCost fun (x : ℕ) (d : Cost.Data) => (d.size + 1) ^ k

(|d| + 1) ^ k is a polynomial cost.

theorem MIPRE.Halting.polyBounded_muZ : Cost.PolyBounded muZ

theorem MIPRE.Halting.polyBounded_eZ (G : GapCompression) (U : Cost.UniversalMachine) (UT : Cost.ClockedUniversalMachine) (S' : Cost.Prog) : Cost.PolyBounded (eZ G U UT S')

theorem MIPRE.Halting.polyBounded_pZ (G : GapCompression) (U : Cost.UniversalMachine) (UT : Cost.ClockedUniversalMachine) (S' : Cost.Prog) : Cost.PolyBounded (pZ G U UT S')

theorem MIPRE.Halting.polyBounded_feZ (G : GapCompression) (U : Cost.UniversalMachine) (UT : Cost.ClockedUniversalMachine) (S' : Cost.Prog) : Cost.PolyBounded (feZ G U UT S')

theorem MIPRE.Halting.polyBounded_sigmaZ (G : GapCompression) (U : Cost.UniversalMachine) (UT : Cost.ClockedUniversalMachine) (S' : Cost.Prog) : Cost.PolyBounded (sigmaZ G U UT S')

theorem MIPRE.Halting.polyBounded_ovZ (G : GapCompression) (U : Cost.UniversalMachine) (UT : Cost.ClockedUniversalMachine) (S' : Cost.Prog) : Cost.PolyBounded (ovZ G U UT S')

theorem MIPRE.Halting.polyCost_vZ : Cost.PolyCost fun (z : ℕ) (d : Cost.Data) => vZ z d.size

theorem MIPRE.Halting.polyCost_tpZ (G : GapCompression) (U : Cost.UniversalMachine) (UT : Cost.ClockedUniversalMachine) (S' : Cost.Prog) : Cost.PolyCost fun (z : ℕ) (d : Cost.Data) => tpZ G U UT S' z d.size

theorem MIPRE.Halting.polyCost_tcZ (G : GapCompression) : Cost.PolyCost fun (z : ℕ) (d : Cost.Data) => tcZ G z d.size

theorem MIPRE.Halting.polyCost_tuZ (G : GapCompression) (U : Cost.UniversalMachine) (UT : Cost.ClockedUniversalMachine) (S' : Cost.Prog) : Cost.PolyCost fun (z : ℕ) (d : Cost.Data) => tuZ G U UT S' z d.size

theorem MIPRE.Halting.polyCost_tbZ (G : GapCompression) (U : Cost.UniversalMachine) (UT : Cost.ClockedUniversalMachine) (S' : Cost.Prog) : Cost.PolyCost fun (z : ℕ) (d : Cost.Data) => tbZ G U UT S' z d.size

theorem MIPRE.Halting.polyCost_tfZ (G : GapCompression) (U : Cost.UniversalMachine) (UT : Cost.ClockedUniversalMachine) (S' : Cost.Prog) : Cost.PolyCost fun (z : ℕ) (d : Cost.Data) => tfZ G U UT S' z d.size

theorem MIPRE.Halting.polyCost_decRunZ (G : GapCompression) (U : Cost.UniversalMachine) (UT : Cost.ClockedUniversalMachine) (S' : Cost.Prog) : Cost.PolyCost fun (z : ℕ) (d : Cost.Data) => decRunZ G U UT S' z d.size

theorem MIPRE.Halting.exists_dec_cost_poly (G : GapCompression) (U : Cost.UniversalMachine) (UT : Cost.ClockedUniversalMachine) (S' : Cost.Prog) : ∃ (Q : Polynomial ℕ) (k : ℕ), ∀ (M : Cost.Prog) (lam n : ℕ) (d : Cost.Data), ∃ (r : Cost.Data), ∃ t ≤ Polynomial.eval (n + Cost.esize M + lam) Q * (d.size + 1) ^ k, (dec G U UT S' M lam).Runs ((Cost.encode n).cons d) r t

The decider's cost, in polynomial form: a polynomial Q and a degree k, depending on G, U, UT and S' alone, with dec M λ halting on (n, d) within Q (n + |M| + λ) · (|d| + 1) ^ k.

noncomputable def MIPRE.Halting.decCostPoly (G : GapCompression) (U : Cost.UniversalMachine) (UT : Cost.ClockedUniversalMachine) (S' : Cost.Prog) : Polynomial ℕ

The polynomial of the decider's cost.

Equations

• MIPRE.Halting.decCostPoly G U UT S' = ⋯.choose

noncomputable def MIPRE.Halting.decCostDeg (G : GapCompression) (U : Cost.UniversalMachine) (UT : Cost.ClockedUniversalMachine) (S' : Cost.Prog) : ℕ

The degree of the decider's cost in the input size.

Equations

• MIPRE.Halting.decCostDeg G U UT S' = ⋯.choose

theorem MIPRE.Halting.dec_cost_spec (G : GapCompression) (U : Cost.UniversalMachine) (UT : Cost.ClockedUniversalMachine) (S' M : Cost.Prog) (lam n : ℕ) (d : Cost.Data) : ∃ (r : Cost.Data), ∃ t ≤ Polynomial.eval (n + Cost.esize M + lam) (decCostPoly G U UT S') * (d.size + 1) ^ decCostDeg G U UT S', (dec G U UT S' M lam).Runs ((Cost.encode n).cons d) r t

The wrapped decider

theorem MIPRE.Halting.Vhalt_decider_cost (G : GapCompression) (U : Cost.UniversalMachine) (UT : Cost.ClockedUniversalMachine) (S' M : Cost.Prog) (lam n : ℕ) (d : Cost.Data) : ∃ (r : Cost.Data), ∃ t ≤ Cost.Prog.wrapCoreCost U (G.sampler lam) (dec G U UT S' M lam) (fun (m : ℕ) => Polynomial.eval (m + lam) G.bound) G.deg n (Polynomial.eval (n + Cost.esize M + lam) (decCostPoly G U UT S') * (d.size + 1) ^ decCostDeg G U UT S') d.size, (Vhalt G U UT S' M lam).decider.prog.Runs ((Cost.encode n).cons d) r t

The decider of 𝒱^halt, on every input: the wrapper's cost with the inner cost in polynomial form.

theorem MIPRE.Halting.esize_sampler_prog_le (G : GapCompression) (lam : ℕ) : Cost.esize (G.sampler lam).prog ≤ Polynomial.eval (Cost.esize lam) G.samplerProg.timeBound

The compressed sampler's program at λ has size at most samplerProg's time bound at |λ|.

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

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

Equations

• MIPRE.Halting.sampSizeZ G z = Polynomial.eval (MIPRE.Halting.muZ z) G.samplerProg.timeBound

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

The compressor's bound poly(m, λ), in z.

Equations

• MIPRE.Halting.betaZ G z = Polynomial.eval (2 * z) G.bound

noncomputable def MIPRE.Halting.headWZ (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.WZ (G : GapCompression) (U : Cost.UniversalMachine) (UT : Cost.ClockedUniversalMachine) (S' : Cost.Prog) (z : ℕ) : ℕ

The master bound on the wrapped decider's cost, in z: wrapCoreCost with every atom replaced by its bound.

Equations

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

theorem MIPRE.Halting.polyBounded_sampSizeZ (G : GapCompression) : Cost.PolyBounded (sampSizeZ G)

theorem MIPRE.Halting.polyBounded_betaZ (G : GapCompression) : Cost.PolyBounded (betaZ G)

theorem MIPRE.Halting.polyBounded_headWZ (G : GapCompression) (U : Cost.UniversalMachine) : Cost.PolyBounded (headWZ G U)

theorem MIPRE.Halting.polyBounded_WZ (G : GapCompression) (U : Cost.UniversalMachine) (UT : Cost.ClockedUniversalMachine) (S' : Cost.Prog) : Cost.PolyBounded (WZ G U UT S')

theorem MIPRE.Halting.wrapCoreCost_le_WZ (G : GapCompression) (U : Cost.UniversalMachine) (UT : Cost.ClockedUniversalMachine) (S' M : Cost.Prog) {lam m s z : ℕ} (hM : Cost.esize M ≤ z) (hm : m ≤ z) (hl : lam ≤ z) (hs : s ≤ z) : Cost.Prog.wrapCoreCost U (G.sampler lam) (dec G U UT S' M lam) (fun (m : ℕ) => Polynomial.eval (m + lam) G.bound) G.deg m (Polynomial.eval (m + Cost.esize M + lam) (decCostPoly G U UT S') * (s + 1) ^ decCostDeg G U UT S') s ≤ WZ G U UT S' z

The wrapped decider's cost is below the master bound at any z above the index, |M|, λ and the input size.

The clauses of IsBounded

theorem MIPRE.Halting.sampler_clauses_paper (G : GapCompression) : ∃ (n₀ : ℕ), ∀ (lam : ℕ), n₀ ≤ lam → ∀ (m : ℕ), 2 ≤ m → Polynomial.eval (m + lam) G.bound ≤ m ^ lam ∧ (G.sampler lam).dim m ≤ m ^ lam ∧ (G.sampler lam).TimeBoundAt m (m ^ lam) lam

The sampler clauses and the parameter inequality: past a threshold on λ, at every index m ≥ 2 the compressor's bound poly(m, λ) is below m ^ λ, so the compressed sampler at λ has dimension at most m ^ λ and runs within m ^ λ · (|d| + 1) ^ λ.

theorem MIPRE.Halting.decider_clause_paper (G : GapCompression) (U : Cost.UniversalMachine) (UT : Cost.ClockedUniversalMachine) (S' : Cost.Prog) : ∃ (n₀ : ℕ), ∀ (M : Cost.Prog) (lam : ℕ), n₀ ≤ lam → Cost.esize M ≤ lam → ∀ (m : ℕ), 2 ≤ m → (Vhalt G U UT S' M lam).decider.TimeBoundAt m (m ^ lam) lam

The decider clause: past a threshold on λ, for |M| ≤ λ, the decider of 𝒱^halt runs within m ^ λ · (|d| + 1) ^ λ at every index m ≥ 2.

noncomputable def MIPRE.Halting.vsizeZ (G : GapCompression) (U : Cost.UniversalMachine) (UT : Cost.ClockedUniversalMachine) (S' : Cost.Prog) (l : ℕ) : ℕ

The size of 𝒱^halt beyond 2|M|, as a function of |λ|.

Equations

• MIPRE.Halting.vsizeZ G U UT S' l = Polynomial.eval l G.samplerProg.timeBound + 2 * l + (MIPRE.Halting.cD G U UT S' + 2 * MIPRE.Cost.esize U.univ + MIPRE.Cost.Prog.ProgD.wrapNodes)

theorem MIPRE.Halting.polyBounded_vsizeZ (G : GapCompression) (U : Cost.UniversalMachine) (UT : Cost.ClockedUniversalMachine) (S' : Cost.Prog) : Cost.PolyBounded (vsizeZ G U UT S')

theorem MIPRE.Halting.Vhalt_size_le (G : GapCompression) (U : Cost.UniversalMachine) (UT : Cost.ClockedUniversalMachine) (S' M : Cost.Prog) (lam : ℕ) : (Vhalt G U UT S' M lam).size ≤ 2 * Cost.esize M + vsizeZ G U UT S' (Cost.esize lam)

The size of 𝒱^halt M λ is at most 2|M| + vsizeZ |λ|.

theorem MIPRE.Halting.size_clause_paper (G : GapCompression) (U : Cost.UniversalMachine) (UT : Cost.ClockedUniversalMachine) (S' : Cost.Prog) : ∃ (n₀ : ℕ), ∀ (M : Cost.Prog) (lam : ℕ), n₀ ≤ lam → 4 * Cost.esize M ≤ lam → (Vhalt G U UT S' M lam).size ≤ lam

The size clause: past a threshold on λ, for 4|M| ≤ λ, |𝒱^halt M λ| ≤ λ.

lem:lambda

theorem MIPRE.Halting.exists_lamBound (G : GapCompression) (U : Cost.UniversalMachine) (UT : Cost.ClockedUniversalMachine) (S' : Cost.Prog) : ∃ (Λ₀ : ℕ), ∀ (M : Cost.Prog) (lam : ℕ), Λ₀ + 4 * Cost.esize M ≤ lam → (Vhalt G U UT S' M lam).IsBounded lam ∧ ∀ (n : ℕ), 2 ≤ n → Polynomial.eval (n + lam) G.bound ≤ n ^ lam

lem:lambda, the paper's form: there is a threshold Λ₀, depending on G, U, UT and S' alone, such that for every machine M and every λ ≥ Λ₀ + 4|M|, the verifier 𝒱^halt M λ is λ-bounded and the compressor's bound poly(n, λ) is below n ^ λ at every level n ≥ 2.

noncomputable def MIPRE.Halting.Lam0 (G : GapCompression) (U : Cost.UniversalMachine) (UT : Cost.ClockedUniversalMachine) (S' : Cost.Prog) : ℕ

The threshold of lem:lambda.

Equations

• MIPRE.Halting.Lam0 G U UT S' = ⋯.choose

theorem MIPRE.Halting.Lam0_spec (G : GapCompression) (U : Cost.UniversalMachine) (UT : Cost.ClockedUniversalMachine) (S' M : Cost.Prog) (lam : ℕ) (h : Lam0 G U UT S' + 4 * Cost.esize M ≤ lam) : (Vhalt G U UT S' M lam).IsBounded lam ∧ ∀ (n : ℕ), 2 ≤ n → Polynomial.eval (n + lam) G.bound ≤ n ^ lam