From polynomially bounded cost to λ-boundedness

Verifier.IsBounded (blueprint def:lambda-bounded) is the hypothesis every class membership of the halting reduction carries, and until this file nothing in the repository inhabited it: every proof of it was conditional on another time bound. This file closes that gap in the abstract, leaving exactly one thing to supply — that the two programs of the verifier have polynomially bounded cost (Prog.HasPolyCost).

• Verifier.IsBounded.mono: λ-boundedness is monotone in λ. The classes classA n, classB n ask for IsBounded n at the level n itself, so a verifier bounded at some λ is in them from λ on; this is what the thresholds n₀ of MIPRE.Halting.Obligations absorb.
• Decider.timeBoundAt_of_hasPolyCost and CL.Sampler.timeBoundAt_of_hasPolyCost: a cost C n · (|d| + 1) ^ k with C polynomially bounded fits under n ^ λ · (|d| + 1) ^ λ for a single λ and every n ≥ 2 (PolyBounded.exists_le_pow). This is the step that the two repairs of TimeBoundAt (#57, #61) were about: the bound has to grow with the input, and its degree has to be free, or nothing that calls the universal machine can meet it.
• Verifier.exists_isBounded: the threshold form, ∃ n₀, ∀ n ≥ n₀, V.IsBounded n, which is what the classes consume.

Nothing here knows about wrappers or descriptions; Halting/WrapperCost.lean discharges the HasPolyCost hypotheses for the verifier a string denotes.

Monotonicity in λ

theorem MIPRE.Verifier.IsBounded.mono {ℓ : ℕ} {V : Verifier ℓ} {lam lam' : ℕ} (h : V.IsBounded lam) (hle : lam ≤ lam') : V.IsBounded lam'

λ-boundedness is monotone in λ: every clause of def:lambda-bounded weakens as λ grows. Raising λ is free, which is what lets a verifier bounded at some fixed λ belong to the classes at every level above it.

Polynomially bounded cost gives a time bound

theorem MIPRE.Cost.Prog.HasPolyCost.exists_bound {p : Prog} (h : p.HasPolyCost) : ∃ (lam : ℕ), ∀ (n : ℕ), 2 ≤ n → ∀ (d : Data), HaltsWithin p ((encode n).cons d) (n ^ lam * (d.size + 1) ^ lam)

A program of polynomially bounded cost meets a single n ^ λ time bound at degree λ, for every n ≥ 2. The degree and the coefficient are chosen together: PolyBounded.exists_le_pow supplies a λ above which the coefficient fits under n ^ λ, and the degree of the cost is absorbed by raising λ further.

theorem MIPRE.Decider.timeBoundAt_of_hasPolyCost {D : Decider} (h : D.prog.HasPolyCost) : ∃ (lam : ℕ), ∀ (n : ℕ), 2 ≤ n → D.TimeBoundAt n (n ^ lam) lam

The decider form of Prog.HasPolyCost.exists_bound.

theorem MIPRE.CL.Sampler.timeBoundAt_of_hasPolyCost {ℓ : ℕ} {S : Sampler ℓ} (h : S.prog.HasPolyCost) : ∃ (lam : ℕ), ∀ (n : ℕ), 2 ≤ n → S.TimeBoundAt n (n ^ lam) lam

The sampler form of Prog.HasPolyCost.exists_bound.

The converse: a time bound with a polynomially bounded coefficient

theorem MIPRE.Cost.Prog.hasPolyCost_of_bound {p : Prog} {T : ℕ → ℕ} {k : ℕ} (hT : PolyBounded T) (h : ∀ (n : ℕ) (d : Data), HaltsWithin p ((encode n).cons d) (T n * (d.size + 1) ^ k)) : p.HasPolyCost

A uniform time bound whose coefficient is polynomially bounded is polynomially bounded cost. This is the direction MIPRE.GapCompression supplies: its sampler_time and decider_time fields bound the running times of the compressed verifier by bound.eval (n + λ) at a fixed degree, and bound.eval (n + λ) is polynomially bounded in n.

theorem MIPRE.CL.Sampler.hasPolyCost_of_timeBound {ℓ : ℕ} {S : Sampler ℓ} {T : ℕ → ℕ} {k : ℕ} (hT : Cost.PolyBounded T) (h : ∀ (n : ℕ), S.TimeBoundAt n (T n) k) : S.prog.HasPolyCost

The sampler form.

λ-boundedness of a verifier

theorem MIPRE.Verifier.exists_isBounded_lam {ℓ : ℕ} (V : Verifier ℓ) (hdim : Cost.PolyBounded V.sampler.dim) (hS : V.sampler.prog.HasPolyCost) (hD : V.decider.prog.HasPolyCost) : ∃ (lam : ℕ), V.IsBounded lam

A verifier whose programs have polynomially bounded cost and whose sampler has polynomially bounded dimension is λ-bounded, for some λ. The three hypotheses are the three clauses of def:lambda-bounded; the fourth, |𝒱| ≤ λ, is free, the size of a verifier being a constant.

theorem MIPRE.Verifier.exists_isBounded {ℓ : ℕ} (V : Verifier ℓ) (hdim : Cost.PolyBounded V.sampler.dim) (hS : V.sampler.prog.HasPolyCost) (hD : V.decider.prog.HasPolyCost) : ∃ (n₀ : ℕ), ∀ (n : ℕ), n₀ ≤ n → V.IsBounded n

The threshold form: such a verifier is n-bounded at every level n from some n₀ on. This is the shape the classes MIPRE.Halting.classA, classB consume, IsBounded n being asked at the level itself.