The complexity clause of the answer reduction

Slice P4h of planning/aldous-lyons-track.md, concluded: the output verifier of the answer reduction (ArRoutine.output) is within the contract's output budget (TailoredAnswerReduction.within): an input within inBudget λ μ n with |𝒱| ≤ σ gives an output whose sampler, calculator and processor run within outBound bound λ μ σ n at degree outDegree deg μ, whose questions have dimension and whose lengths are at most the same bound, for a polynomial bound and a degree deg depending only on the routine (output_within), under the one hypothesis that the routine's parameter program runs in polynomial time (ArRoutine.ParTime). The calculator halting on every input, the contract's len_total, is ArRoutine.lenD_total.

theorem MIPRE.Tailored.AnsRed.Typed.pow_le_pow_of_le' {W K c m C M : ℕ} (hc : c ≤ C) (hm : m ≤ M) : (c * (W + 1) ^ m) ^ (K + 1) ≤ (C * (W + 1) ^ M) ^ (K + 1)

A monomial bound below a larger one.

theorem MIPRE.Tailored.AnsRed.Typed.ArRoutine.output_within {R : ArRoutine} (hR : R.ParTime) (ℓ : ℕ) : ∃ (bound : Polynomial ℕ) (deg : ℕ), ∀ (V : TailoredVerifier (ℓ + 1)) (lam mu sigma n : ℕ), V.Within n (AnswerReduction.inBudget lam mu n) → V.size ≤ sigma → (R.output V lam mu sigma).Within n (Budget.uniform (AnswerReduction.outBound bound lam mu sigma n) (AnswerReduction.outDegree deg mu))

The complexity clause of the answer reduction (TailoredAnswerReduction.within): an input within inBudget λ μ n with |𝒱| ≤ σ gives an output within outBound bound λ μ σ n at degree outDegree deg μ, for a polynomial bound and a degree deg depending only on the routine.