Polynomially bounded functions

The time accounting of the instantiation (Halting/Wrapper.lean, Halting/Compressor.lean) composes a dozen explicit cost bounds, each a polynomial in the values it depends on. What the argument eventually needs is only that the total is bounded by some polynomial in the level, so that it falls under 2 ^ n above a threshold. PolyBounded f records exactly that — f n ≤ P.eval n for some P : Polynomial ℕ — with the closure properties that let the bounds be composed without ever writing the polynomial down:

• constants, the identity, sums, products, powers, Nat.size;
• PolyBounded.comp: a polynomially bounded function of a polynomially bounded function;
• PolyBounded.eval: a fixed polynomial evaluated at a polynomially bounded argument;
• PolyBounded.mono: domination by a polynomially bounded function;
• PolyBounded.exists_le_two_pow: the threshold, f n ≤ 2 ^ n for all n above some n₀; PolyBounded.exists_le_pow: a single λ with f n ≤ n ^ λ for every n ≥ 2, which is the shape Verifier.IsBounded asks for.

PolyCost and HasPolyCost are the same notion for the cost of a program at index n on an input d: bounded by C n · (|d| + 1) ^ k with C polynomially bounded and k constant — exactly what Decider.TimeBoundAt asks for, and what the stages of a decider's run compose into (PolyCost.add, mul, poly, the last being the universal machine's overhead).

The polynomial of a PolyBounded function can be extracted (PolyBounded.choose) where an explicit Polynomial ℕ is required, as in the timeBound field of PolyTimeFun.

def MIPRE.Cost.PolyBounded (f : ℕ → ℕ) : Prop

f is bounded by a polynomial.

Equations

• MIPRE.Cost.PolyBounded f = ∃ (P : Polynomial ℕ), ∀ (n : ℕ), f n ≤ Polynomial.eval n P

theorem MIPRE.Cost.PolyBounded.const (c : ℕ) : PolyBounded fun (x : ℕ) => c

theorem MIPRE.Cost.PolyBounded.id : PolyBounded fun (n : ℕ) => n

theorem MIPRE.Cost.PolyBounded.mono {f g : ℕ → ℕ} (hg : PolyBounded g) (h : ∀ (n : ℕ), f n ≤ g n) : PolyBounded f

theorem MIPRE.Cost.PolyBounded.add {f g : ℕ → ℕ} (hf : PolyBounded f) (hg : PolyBounded g) : PolyBounded fun (n : ℕ) => f n + g n

theorem MIPRE.Cost.PolyBounded.mul {f g : ℕ → ℕ} (hf : PolyBounded f) (hg : PolyBounded g) : PolyBounded fun (n : ℕ) => f n * g n

theorem MIPRE.Cost.PolyBounded.pow {f : ℕ → ℕ} (hf : PolyBounded f) (k : ℕ) : PolyBounded fun (n : ℕ) => f n ^ k

theorem MIPRE.Cost.PolyBounded.const_mul {f : ℕ → ℕ} (c : ℕ) (hf : PolyBounded f) : PolyBounded fun (n : ℕ) => c * f n

theorem MIPRE.Cost.PolyBounded.add_const {f : ℕ → ℕ} (hf : PolyBounded f) (c : ℕ) : PolyBounded fun (n : ℕ) => f n + c

theorem MIPRE.Cost.PolyBounded.eval (P : Polynomial ℕ) {f : ℕ → ℕ} (hf : PolyBounded f) : PolyBounded fun (n : ℕ) => Polynomial.eval (f n) P

A fixed polynomial at a polynomially bounded argument.

theorem MIPRE.Cost.PolyBounded.comp {g f : ℕ → ℕ} (hg : PolyBounded g) (hf : PolyBounded f) : PolyBounded fun (n : ℕ) => g (f n)

A polynomially bounded function of a polynomially bounded argument. Polynomials over ℕ are monotone, so no monotonicity of g is needed.

theorem MIPRE.Cost.PolyBounded.size : PolyBounded Nat.size

theorem MIPRE.Cost.PolyBounded.two_mul_add_one : PolyBounded fun (n : ℕ) => 2 * n + 1

noncomputable def MIPRE.Cost.PolyBounded.poly {f : ℕ → ℕ} (hf : PolyBounded f) : Polynomial ℕ

The polynomial of a polynomially bounded function.

Equations

• hf.poly = Exists.choose hf

theorem MIPRE.Cost.PolyBounded.le_poly_eval {f : ℕ → ℕ} (hf : PolyBounded f) (n : ℕ) : f n ≤ Polynomial.eval n hf.poly

theorem MIPRE.Cost.PolyBounded.exists_le_two_pow {f : ℕ → ℕ} (hf : PolyBounded f) : ∃ (n₀ : ℕ), ∀ (n : ℕ), n₀ ≤ n → f n ≤ 2 ^ n

The threshold. A polynomially bounded function is below 2 ^ n from some n₀ on.

theorem MIPRE.Cost.PolyBounded.exists_le_pow {f : ℕ → ℕ} (hf : PolyBounded f) : ∃ (lam : ℕ), ∀ (n : ℕ), 2 ≤ n → f n ≤ n ^ lam

A single exponent for every index. A polynomially bounded function is below n ^ λ for one λ and all n ≥ 2 — the form Verifier.IsBounded asks for.

theorem MIPRE.Cost.polyBounded_esize_nat : PolyBounded fun (n : ℕ) => esize n

The size of the binary encoding of n is polynomially bounded.

Costs, polynomially bounded in the index and in the input

def MIPRE.Cost.PolyCost (f : ℕ → Data → ℕ) : Prop

A cost function of an index and an input, bounded by C n · (|d| + 1) ^ k with C polynomially bounded and k constant.

Equations

• MIPRE.Cost.PolyCost f = ∃ (C : ℕ → ℕ) (k : ℕ), MIPRE.Cost.PolyBounded C ∧ ∀ (n : ℕ) (d : MIPRE.Cost.Data), f n d ≤ C n * (d.size + 1) ^ k

theorem MIPRE.Cost.PolyCost.mono {f g : ℕ → Data → ℕ} (hg : PolyCost g) (h : ∀ (n : ℕ) (d : Data), f n d ≤ g n d) : PolyCost f

theorem MIPRE.Cost.PolyCost.const (c : ℕ) : PolyCost fun (x : ℕ) (x_1 : Data) => c

theorem MIPRE.Cost.PolyCost.ofIndex {g : ℕ → ℕ} (hg : PolyBounded g) : PolyCost fun (n : ℕ) (x : Data) => g n

theorem MIPRE.Cost.PolyCost.size : PolyCost fun (x : ℕ) (d : Data) => d.size

theorem MIPRE.Cost.PolyCost.add {f g : ℕ → Data → ℕ} (hf : PolyCost f) (hg : PolyCost g) : PolyCost fun (n : ℕ) (d : Data) => f n d + g n d

theorem MIPRE.Cost.PolyCost.mul {f g : ℕ → Data → ℕ} (hf : PolyCost f) (hg : PolyCost g) : PolyCost fun (n : ℕ) (d : Data) => f n d * g n d

theorem MIPRE.Cost.PolyCost.poly (P : Polynomial ℕ) {f : ℕ → Data → ℕ} (hf : PolyCost f) : PolyCost fun (n : ℕ) (d : Data) => Polynomial.eval (f n d) P

A fixed polynomial at a polynomially bounded cost: the universal machine's overhead.

def MIPRE.Cost.Prog.HasPolyCost (p : Prog) : Prop

A program whose cost at index n on input d is polynomially bounded: the hypothesis the deciders of the instantiation carry, and (through hasPolyCost_iff_exists_isBounded) what λ-boundedness comes from.

Equations

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

theorem MIPRE.Cost.Prog.hasPolyCost_of_polyCost {p : Prog} {B : ℕ → Data → ℕ} (hB : PolyCost B) (h : ∀ (n : ℕ) (d : Data), ∃ (r : Data), ∃ t ≤ B n d, p.Runs ((encode n).cons d) r t) : p.HasPolyCost

A cost bound of the composable shape PolyCost is a HasPolyCost: the two differ only in whether the polynomial in the input size is displayed. Cost analyses are assembled in the first form, where add, mul and poly apply, and consumed in the second.