Domination by a power of a monomial

The time bounds of the answer-reduced verifier (thm:answer-reduction) have the shape (c (W + 1)^m X^e)^{K + 1}: W a number dominating the parameters at index n, X = |d| + 1 the size of the input and K = μ the input sampler's degree. It is the shape of the contract's outBound bound λ μ σ n = P(L + σ)^{μ + 1} at degree d (μ + 1): one call to a sampler of coefficient B ≤ W and degree K on a query of size below c (W + 1)^m X^e costs B (c (W + 1)^m X^e)^K, which is of this shape (ofCall), and so is any fixed polynomial of such a cost (poly). MIPRE.Repeat.Dom is the unpowered shape c (W + 1)^m X^{e (K + 1)}, which suffices when the coefficient of the simulated program does not depend on K; here the powered coefficient carries the constants that a query larger than the input by a constant factor raises to the power K, and the index-independent K + 1 ≤ 2^{K + 1} (ofLeK).

PDom W X K c m e v says v is below (c (W + 1)^m X^e)^{K + 1}; the combinators assemble the constants, and le_final reads off the coefficient (c (W + 1)^m)^{K + 1} and degree e (K + 1).

def MIPRE.Pipeline.PDom (W X K c m e v : ℕ) : Prop

v ≤ (c (W + 1)^m X^e)^{K + 1}.

Equations

• MIPRE.Pipeline.PDom W X K c m e v = (v ≤ (c * (W + 1) ^ m * X ^ e) ^ (K + 1))

theorem MIPRE.Pipeline.PDom.of_le {W X K c m e v v' : ℕ} (h : PDom W X K c m e v) (hv : v' ≤ v) : PDom W X K c m e v'

theorem MIPRE.Pipeline.PDom.le_final {W X K c m e v : ℕ} (h : PDom W X K c m e v) : v ≤ (c * (W + 1) ^ m) ^ (K + 1) * X ^ (e * (K + 1))

The coefficient and the degree.

theorem MIPRE.Pipeline.PDom.mono {W X K : ℕ} (hX : 1 ≤ X) {c c' m m' e e' v : ℕ} (h : PDom W X K c m e v) (hc : c ≤ c') (hm : m ≤ m') (he : e ≤ e') : PDom W X K c' m' e' v

theorem MIPRE.Pipeline.PDom.le_pow_succ {K a : ℕ} : a ≤ a ^ (K + 1)

A base of at least one is below its (K + 1)-st power.

theorem MIPRE.Pipeline.PDom.const {W X K : ℕ} (c : ℕ) : PDom W X K (c + 1) 0 0 c

theorem MIPRE.Pipeline.PDom.ofLeW {W X K v : ℕ} (h : v ≤ W) : PDom W X K 1 1 0 v

theorem MIPRE.Pipeline.PDom.ofAffine {W X K a b v : ℕ} (h : v ≤ a * W + b) : PDom W X K (a + b + 1) 1 0 v

An affine function of W.

theorem MIPRE.Pipeline.PDom.ofLeX {W X K v : ℕ} (h : v ≤ X) : PDom W X K 1 0 1 v

theorem MIPRE.Pipeline.PDom.ofLeK {W X K v : ℕ} (h : v ≤ K + 1) : PDom W X K 2 0 0 v

K + 1 ≤ 2^{K + 1}: the input sampler's degree itself is dominated.

theorem MIPRE.Pipeline.PDom.add {W X K : ℕ} (hX : 1 ≤ X) {c₁ c₂ m₁ m₂ e₁ e₂ v₁ v₂ : ℕ} (h₁ : PDom W X K c₁ m₁ e₁ v₁) (h₂ : PDom W X K c₂ m₂ e₂ v₂) : PDom W X K (c₁ + c₂) (max m₁ m₂) (max e₁ e₂) (v₁ + v₂)

theorem MIPRE.Pipeline.PDom.mul {W X K c₁ c₂ m₁ m₂ e₁ e₂ v₁ v₂ : ℕ} (h₁ : PDom W X K c₁ m₁ e₁ v₁) (h₂ : PDom W X K c₂ m₂ e₂ v₂) : PDom W X K (c₁ * c₂) (m₁ + m₂) (e₁ + e₂) (v₁ * v₂)

theorem MIPRE.Pipeline.PDom.pow {W X K c m e v : ℕ} (h : PDom W X K c m e v) (p : ℕ) : PDom W X K (c ^ p) (m * p) (e * p) (v ^ p)

theorem MIPRE.Pipeline.PDom.poly {W X K : ℕ} (hX : 1 ≤ X) (P : Polynomial ℕ) {c m e y : ℕ} (h : PDom W X K c m e y) : PDom W X K ((∑ i ∈ Finset.range (P.natDegree + 1), P.coeff i + 1) * (c + 2) ^ P.natDegree) (m * P.natDegree) (e * P.natDegree) (Polynomial.eval y P)

A fixed polynomial of a dominated quantity.

theorem MIPRE.Pipeline.PDom.ofCall {W X K B q t c m e : ℕ} (hB : B ≤ W) (hq : q + 1 ≤ c * (W + 1) ^ m * X ^ e) (ht : t ≤ B * (q + 1) ^ K) : PDom W X K c (m + 1) e t

One call to a sampler of coefficient B ≤ W and degree K, on a query of size below the unpowered monomial c (W + 1)^m X^e.

theorem MIPRE.Pipeline.PDom.ofCallPow {W X K B q t c₀ m₀ c₁ m₁ e₁ e' : ℕ} (hB : B ≤ c₀ * (W + 1) ^ m₀) (hq : q + 1 ≤ c₁ * (W + 1) ^ m₁ * X ^ e₁) (ht : t ≤ B * (q + 1) ^ (e' * (K + 1))) : PDom W X K (c₀ * c₁ ^ e') (m₀ + m₁ * e') (e₁ * e') t

One call to a program of coefficient B ≤ c₀ (W + 1)^{m₀} and degree e' (K + 1), on a query of size below the unpowered monomial c₁ (W + 1)^{m₁} X^{e₁}.

theorem MIPRE.Pipeline.PDom.ofPoweredCall {W X K B q t c₀ m₀ c₁ m₁ e₁ e' : ℕ} (hB : B ≤ (c₀ * (W + 1) ^ m₀) ^ (K + 1)) (hq : q ≤ c₁ * (W + 1) ^ m₁ * X ^ e₁) (ht : t ≤ B * q ^ (e' * (K + 1))) : PDom W X K (c₀ * c₁ ^ e') (m₀ + m₁ * e') (e₁ * e') t

A run of a program whose coefficient is already powered, B ≤ (c₀ (W + 1)^{m₀})^{K + 1}, at degree e' (K + 1), on an input of size below the unpowered monomial c₁ (W + 1)^{m₁} X^{e₁}.

theorem MIPRE.Pipeline.PDom.ofMono {W X K c m e v : ℕ} (h : v ≤ c * (W + 1) ^ m * X ^ e) : PDom W X K c m e v

Below the unpowered monomial.

theorem MIPRE.Pipeline.PDom.ofLin {W X K : ℕ} (hX : 1 ≤ X) {a b c v : ℕ} (h : v ≤ a * W + b * (K + 1) + c) : PDom W X K (a + 2 * b + c + 3) 1 0 v

A linear function of W and K + 1.