The tailored halting verifier: the accounting

Paper II, lem:lambda (II:2002), for the three programs of a tailored verifier, along the route of MIPRE/Foundations/Halting/Paper/{Size,Cost}.lean, which this file parallels: the verifier Vhalt M λ is λ-bounded (TailoredVerifier.IsBounded λ) as soon as λ ≥ Λ₀ + 4|M|, for a threshold Λ₀ depending on the compression, the universal machines and the search program alone (exists_lamBound, Lam0).

• Sizes (esize_lpProg): the processor lp M λ is a hardcoding of the fixed point's program to its own description, so its size is 2 (|M| + |λ|) plus a constant — the reason the parameter is Λ₀ + 4|M|.
• The processor's run (lp_cost): on (n, d), lp M λ runs within lpRunZ z |d| at z = n + |M| + λ, assembled along the fixed point's time transfer (Cost.kleeneFix_runs_of), the hardcoding of the description, the run of prep, the universal machine on what prep returns, and the compressed processor's own time (TailoredGapCompression.lp_time). The existing halting verifier then wraps its decider in the question-length check; a processor is run as it is, so there is no wrapper layer here.
• The clauses of IsBounded λ, each absorbed past a threshold (PolyBounded.absorb, PolyBounded.absorb_log): the sampler's dimension and time and the answer-length calculator's time and lengths, all from the compression's poly(n, λ); the processor's time; and the size.

Sizes

noncomputable def MIPRE.Tailored.Halting.cF {ℓ : ℕ} (TG : TailoredGapCompression ℓ) (U : Cost.UniversalMachine) (UT : Cost.ClockedUniversalMachine) (S' : Cost.Prog) : ℕ

The size of the code of F beyond |M| + |λ|.

Equations

• MIPRE.Tailored.Halting.cF TG U UT S' = MIPRE.Cost.esize (MIPRE.Tailored.Halting.body TG U UT S') + MIPRE.Cost.esize MIPRE.Cost.smnProg + 77

theorem MIPRE.Tailored.Halting.esize_F_code {ℓ : ℕ} (TG : TailoredGapCompression ℓ) (U : Cost.UniversalMachine) (UT : Cost.ClockedUniversalMachine) (S' M : Cost.Prog) (lam : ℕ) : Cost.esize (F TG U UT S' M lam).code = Cost.esize M + Cost.esize lam + cF TG U UT S'

noncomputable def MIPRE.Tailored.Halting.cK {ℓ : ℕ} (TG : TailoredGapCompression ℓ) (U : Cost.UniversalMachine) (UT : Cost.ClockedUniversalMachine) (S' : Cost.Prog) : ℕ

The size of kleeneProg U.univ F beyond |M| + |λ|.

Equations

• MIPRE.Tailored.Halting.cK TG U UT S' = MIPRE.Tailored.Halting.cF TG U UT S' + MIPRE.Cost.esize U.univ + MIPRE.Cost.esize MIPRE.Cost.smnProg + 136

theorem MIPRE.Tailored.Halting.esize_kleeneProg_F {ℓ : ℕ} (TG : TailoredGapCompression ℓ) (U : Cost.UniversalMachine) (UT : Cost.ClockedUniversalMachine) (S' M : Cost.Prog) (lam : ℕ) : Cost.esize (U.univ.kleeneProg (F TG U UT S' M lam)) = Cost.esize M + Cost.esize lam + cK TG U UT S'

noncomputable def MIPRE.Tailored.Halting.cD {ℓ : ℕ} (TG : TailoredGapCompression ℓ) (U : Cost.UniversalMachine) (UT : Cost.ClockedUniversalMachine) (S' : Cost.Prog) : ℕ

The size of the processor lp M λ beyond 2 (|M| + |λ|).

Equations

• MIPRE.Tailored.Halting.cD TG U UT S' = 2 * MIPRE.Tailored.Halting.cK TG U UT S' + 35

theorem MIPRE.Tailored.Halting.esize_lpProg {ℓ : ℕ} (TG : TailoredGapCompression ℓ) (U : Cost.UniversalMachine) (UT : Cost.ClockedUniversalMachine) (S' M : Cost.Prog) (lam : ℕ) : Cost.esize (lpProg TG U UT S' M lam) = 2 * (Cost.esize M + Cost.esize lam) + cD TG U UT S'

theorem MIPRE.Tailored.Halting.esize_F_apply {ℓ : ℕ} (TG : TailoredGapCompression ℓ) (U : Cost.UniversalMachine) (UT : Cost.ClockedUniversalMachine) (S' M : Cost.Prog) (lam : ℕ) (e : Cost.Prog) : Cost.esize ((F TG U UT S' M lam).toFun e) = Cost.esize (body TG U UT S') + Cost.esize M + Cost.esize lam + Cost.esize e + 37

F e = hardcode body (M, (λ, e)) has size |body| + |M| + |λ| + |e| + 37.

theorem MIPRE.Tailored.Halting.F_timeBound_eval {ℓ : ℕ} (TG : TailoredGapCompression ℓ) (U : Cost.UniversalMachine) (UT : Cost.ClockedUniversalMachine) (S' M : Cost.Prog) (lam x : ℕ) : Polynomial.eval x (F TG U UT S' M lam).timeBound = 2 * (Cost.esize (body TG U UT S') + Cost.esize M + Cost.esize lam + x) + 47

The time bound of F: affine in the argument and in |body| + |M| + |λ|.

noncomputable def MIPRE.Tailored.Halting.cO {ℓ : ℕ} (TG : TailoredGapCompression ℓ) (U : Cost.UniversalMachine) (UT : Cost.ClockedUniversalMachine) (S' : Cost.Prog) : ℕ

The overhead of the fixed point's time transfer beyond 21 (|M| + |λ|).

Equations

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

theorem MIPRE.Tailored.Halting.kleeneOverhead_eq {ℓ : ℕ} (TG : TailoredGapCompression ℓ) (U : Cost.UniversalMachine) (UT : Cost.ClockedUniversalMachine) (S' M : Cost.Prog) (lam : ℕ) : Cost.kleeneOverhead U (F TG U UT S' M lam) = 21 * (Cost.esize M + Cost.esize lam) + cO TG U UT S'

What prep returns

def MIPRE.Tailored.Halting.constCost : ℕ

The cost of the two constant programs: the sizes of the two constant outputs.

Equations

• MIPRE.Tailored.Halting.constCost = (MIPRE.Cost.encode []).size + (MIPRE.Cost.encode [MIPRE.Tailored.rejectConstraint 0]).size

noncomputable def MIPRE.Tailored.Halting.progSize {ℓ : ℕ} (TG : TailoredGapCompression ℓ) (lam : ℕ) (e : Cost.Prog) : ℕ

The size of the program prep returns, at the parameter λ and the processor e: the compressed processor'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.Tailored.Halting.prep_output {ℓ : ℕ} (TG : TailoredGapCompression ℓ) (UT : Cost.ClockedUniversalMachine) (S' M : Cost.Prog) (lam : ℕ) (e : Cost.Prog) (n : ℕ) (d : Cost.Data) : Cost.esize ((prep TG UT S').toFun ((M, lam, e), n, d)).1 ≤ progSize TG lam e ∧ ((prep TG UT S').toFun ((M, lam, e), n, d)).2.size ≤ Cost.esize n + d.size + 1 ∧ ∃ (r : Cost.Data), ∃ t ≤ Polynomial.eval (n + lam) TG.bound * (d.size + 1) ^ TG.deg + constCost, ((prep TG UT S').toFun ((M, lam, e), n, d)).1.Runs ((prep TG 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 processor's time plus a constant.

The processor's run

Every atom of the cost — |n|, |M| + |λ|, |λ|, n, λ — is at most muZ z = 5z + 1 or z at z = n + |M| + λ.

noncomputable def MIPRE.Tailored.Halting.eZ {ℓ : ℕ} (TG : TailoredGapCompression ℓ) (U : Cost.UniversalMachine) (UT : Cost.ClockedUniversalMachine) (S' : Cost.Prog) (z : ℕ) : ℕ

The size of the processor, in z.

Equations

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

noncomputable def MIPRE.Tailored.Halting.pZ {ℓ : ℕ} (TG : TailoredGapCompression ℓ) (U : Cost.UniversalMachine) (UT : Cost.ClockedUniversalMachine) (S' : Cost.Prog) (z : ℕ) : ℕ

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

Equations

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

noncomputable def MIPRE.Tailored.Halting.feZ {ℓ : ℕ} (TG : TailoredGapCompression ℓ) (U : Cost.UniversalMachine) (UT : Cost.ClockedUniversalMachine) (S' : Cost.Prog) (z : ℕ) : ℕ

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

Equations

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

noncomputable def MIPRE.Tailored.Halting.tpZ {ℓ : ℕ} (TG : TailoredGapCompression ℓ) (U : Cost.UniversalMachine) (UT : Cost.ClockedUniversalMachine) (S' : Cost.Prog) (z s : ℕ) : ℕ

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

Equations

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

noncomputable def MIPRE.Tailored.Halting.sigmaZ {ℓ : ℕ} (TG : TailoredGapCompression ℓ) (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.Tailored.Halting.tcZ {ℓ : ℕ} (TG : TailoredGapCompression ℓ) (z s : ℕ) : ℕ

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

Equations

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

noncomputable def MIPRE.Tailored.Halting.tuZ {ℓ : ℕ} (TG : TailoredGapCompression ℓ) (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.Tailored.Halting.tuZ TG U UT S' z s = Polynomial.eval (MIPRE.Tailored.Halting.sigmaZ TG U UT S' z + MIPRE.Halting.vZ z s + MIPRE.Tailored.Halting.tcZ TG z s) U.bound

noncomputable def MIPRE.Tailored.Halting.tbZ {ℓ : ℕ} (TG : TailoredGapCompression ℓ) (U : Cost.UniversalMachine) (UT : Cost.ClockedUniversalMachine) (S' : Cost.Prog) (z s : ℕ) : ℕ

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

Equations

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

noncomputable def MIPRE.Tailored.Halting.tfZ {ℓ : ℕ} (TG : TailoredGapCompression ℓ) (U : Cost.UniversalMachine) (UT : Cost.ClockedUniversalMachine) (S' : Cost.Prog) (z s : ℕ) : ℕ

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

Equations

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

noncomputable def MIPRE.Tailored.Halting.ovZ {ℓ : ℕ} (TG : TailoredGapCompression ℓ) (U : Cost.UniversalMachine) (UT : Cost.ClockedUniversalMachine) (S' : Cost.Prog) (z : ℕ) : ℕ

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

Equations

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

noncomputable def MIPRE.Tailored.Halting.lpRunZ {ℓ : ℕ} (TG : TailoredGapCompression ℓ) (U : Cost.UniversalMachine) (UT : Cost.ClockedUniversalMachine) (S' : Cost.Prog) (z s : ℕ) : ℕ

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

Equations

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

theorem MIPRE.Tailored.Halting.lp_cost {ℓ : ℕ} (TG : TailoredGapCompression ℓ) (U : Cost.UniversalMachine) (UT : Cost.ClockedUniversalMachine) (S' M : Cost.Prog) (lam n : ℕ) (d : Cost.Data) : ∃ (r : Cost.Data), ∃ t ≤ lpRunZ TG U UT S' (n + Cost.esize M + lam) d.size, (lpProg TG U UT S' M lam).Runs ((Cost.encode n).cons d) r t

The processor's run: on (n, d), lp M λ halts within lpRunZ (n + |M| + λ) |d|.

The polynomial form

theorem MIPRE.Tailored.Halting.polyBounded_eZ {ℓ : ℕ} (TG : TailoredGapCompression ℓ) (U : Cost.UniversalMachine) (UT : Cost.ClockedUniversalMachine) (S' : Cost.Prog) : Cost.PolyBounded (eZ TG U UT S')

theorem MIPRE.Tailored.Halting.polyBounded_pZ {ℓ : ℕ} (TG : TailoredGapCompression ℓ) (U : Cost.UniversalMachine) (UT : Cost.ClockedUniversalMachine) (S' : Cost.Prog) : Cost.PolyBounded (pZ TG U UT S')

theorem MIPRE.Tailored.Halting.polyBounded_feZ {ℓ : ℕ} (TG : TailoredGapCompression ℓ) (U : Cost.UniversalMachine) (UT : Cost.ClockedUniversalMachine) (S' : Cost.Prog) : Cost.PolyBounded (feZ TG U UT S')

theorem MIPRE.Tailored.Halting.polyBounded_sigmaZ {ℓ : ℕ} (TG : TailoredGapCompression ℓ) (U : Cost.UniversalMachine) (UT : Cost.ClockedUniversalMachine) (S' : Cost.Prog) : Cost.PolyBounded (sigmaZ TG U UT S')

theorem MIPRE.Tailored.Halting.polyBounded_ovZ {ℓ : ℕ} (TG : TailoredGapCompression ℓ) (U : Cost.UniversalMachine) (UT : Cost.ClockedUniversalMachine) (S' : Cost.Prog) : Cost.PolyBounded (ovZ TG U UT S')

theorem MIPRE.Tailored.Halting.polyCost_tpZ {ℓ : ℕ} (TG : TailoredGapCompression ℓ) (U : Cost.UniversalMachine) (UT : Cost.ClockedUniversalMachine) (S' : Cost.Prog) : Cost.PolyCost fun (z : ℕ) (d : Cost.Data) => tpZ TG U UT S' z d.size

theorem MIPRE.Tailored.Halting.polyCost_tcZ {ℓ : ℕ} (TG : TailoredGapCompression ℓ) : Cost.PolyCost fun (z : ℕ) (d : Cost.Data) => tcZ TG z d.size

theorem MIPRE.Tailored.Halting.polyCost_tuZ {ℓ : ℕ} (TG : TailoredGapCompression ℓ) (U : Cost.UniversalMachine) (UT : Cost.ClockedUniversalMachine) (S' : Cost.Prog) : Cost.PolyCost fun (z : ℕ) (d : Cost.Data) => tuZ TG U UT S' z d.size

theorem MIPRE.Tailored.Halting.polyCost_tbZ {ℓ : ℕ} (TG : TailoredGapCompression ℓ) (U : Cost.UniversalMachine) (UT : Cost.ClockedUniversalMachine) (S' : Cost.Prog) : Cost.PolyCost fun (z : ℕ) (d : Cost.Data) => tbZ TG U UT S' z d.size

theorem MIPRE.Tailored.Halting.polyCost_tfZ {ℓ : ℕ} (TG : TailoredGapCompression ℓ) (U : Cost.UniversalMachine) (UT : Cost.ClockedUniversalMachine) (S' : Cost.Prog) : Cost.PolyCost fun (z : ℕ) (d : Cost.Data) => tfZ TG U UT S' z d.size

theorem MIPRE.Tailored.Halting.polyCost_lpRunZ {ℓ : ℕ} (TG : TailoredGapCompression ℓ) (U : Cost.UniversalMachine) (UT : Cost.ClockedUniversalMachine) (S' : Cost.Prog) : Cost.PolyCost fun (z : ℕ) (d : Cost.Data) => lpRunZ TG U UT S' z d.size

theorem MIPRE.Tailored.Halting.exists_lp_cost_poly {ℓ : ℕ} (TG : TailoredGapCompression ℓ) (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, (lpProg TG U UT S' M lam).Runs ((Cost.encode n).cons d) r t

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

The clauses of IsBounded

theorem MIPRE.Tailored.Halting.sampler_len_clauses {ℓ : ℕ} (TG : TailoredGapCompression ℓ) : ∃ (n₀ : ℕ), ∀ (lam : ℕ), n₀ ≤ lam → ∀ (m : ℕ), 2 ≤ m → Polynomial.eval (m + lam) TG.bound ≤ m ^ lam ∧ (TG.sampler lam).dim m ≤ m ^ lam ∧ (TG.sampler lam).TimeBoundAt m (m ^ lam) lam ∧ (TG.len lam).TimeBoundAt m (m ^ lam) lam ∧ LenBound (TG.len lam) m (m ^ lam)

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

theorem MIPRE.Tailored.Halting.lp_clause {ℓ : ℕ} (TG : TailoredGapCompression ℓ) (U : Cost.UniversalMachine) (UT : Cost.ClockedUniversalMachine) (S' : Cost.Prog) : ∃ (n₀ : ℕ), ∀ (M : Cost.Prog) (lam : ℕ), n₀ ≤ lam → Cost.esize M ≤ lam → ∀ (m : ℕ), 2 ≤ m → (Vhalt TG U UT S' M lam).lp.TimeBoundAt m (m ^ lam) lam

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

noncomputable def MIPRE.Tailored.Halting.vsizeZ {ℓ : ℕ} (TG : TailoredGapCompression ℓ) (U : Cost.UniversalMachine) (UT : Cost.ClockedUniversalMachine) (S' : Cost.Prog) (l : ℕ) : ℕ

The size of V^{M,λ} beyond 2|M|, as a function of |λ|.

Equations

• MIPRE.Tailored.Halting.vsizeZ TG U UT S' l = Polynomial.eval l TG.samplerProg.timeBound + Polynomial.eval l TG.lenProg.timeBound + 2 * l + MIPRE.Tailored.Halting.cD TG U UT S'

theorem MIPRE.Tailored.Halting.polyBounded_vsizeZ {ℓ : ℕ} (TG : TailoredGapCompression ℓ) (U : Cost.UniversalMachine) (UT : Cost.ClockedUniversalMachine) (S' : Cost.Prog) : Cost.PolyBounded (vsizeZ TG U UT S')

theorem MIPRE.Tailored.Halting.Vhalt_size_le {ℓ : ℕ} (TG : TailoredGapCompression ℓ) (U : Cost.UniversalMachine) (UT : Cost.ClockedUniversalMachine) (S' M : Cost.Prog) (lam : ℕ) : (Vhalt TG U UT S' M lam).size ≤ 2 * Cost.esize M + vsizeZ TG U UT S' (Cost.esize lam)

The size of V^{M,λ} is at most 2|M| + vsizeZ |λ|.

theorem MIPRE.Tailored.Halting.size_clause {ℓ : ℕ} (TG : TailoredGapCompression ℓ) (U : Cost.UniversalMachine) (UT : Cost.ClockedUniversalMachine) (S' : Cost.Prog) : ∃ (n₀ : ℕ), ∀ (M : Cost.Prog) (lam : ℕ), n₀ ≤ lam → 4 * Cost.esize M ≤ lam → (Vhalt TG U UT S' M lam).size ≤ lam

The size clause: past a threshold on λ, for 4|M| ≤ λ, |V^{M,λ}| ≤ λ.

lem:lambda

theorem MIPRE.Tailored.Halting.exists_lamBound {ℓ : ℕ} (TG : TailoredGapCompression ℓ) (U : Cost.UniversalMachine) (UT : Cost.ClockedUniversalMachine) (S' : Cost.Prog) : ∃ (Λ₀ : ℕ), ∀ (M : Cost.Prog) (lam : ℕ), Λ₀ + 4 * Cost.esize M ≤ lam → (Vhalt TG U UT S' M lam).IsBounded lam

lem:lambda for tailored verifiers: there is a threshold Λ₀, depending on TG, U, UT and S' alone, such that for every machine M and every λ ≥ Λ₀ + 4|M|, the verifier V^{M,λ} is λ-bounded.

noncomputable def MIPRE.Tailored.Halting.Lam0 {ℓ : ℕ} (TG : TailoredGapCompression ℓ) (U : Cost.UniversalMachine) (UT : Cost.ClockedUniversalMachine) (S' : Cost.Prog) : ℕ

The threshold of lem:lambda.

Equations

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

theorem MIPRE.Tailored.Halting.Lam0_spec {ℓ : ℕ} (TG : TailoredGapCompression ℓ) (U : Cost.UniversalMachine) (UT : Cost.ClockedUniversalMachine) (S' M : Cost.Prog) (lam : ℕ) (h : Lam0 TG U UT S' + 4 * Cost.esize M ≤ lam) : (Vhalt TG U UT S' M lam).IsBounded lam