The output's sampler within the budget at λ

The output tailored verifier at λ has the introspection verifier's sampler at Cλ, which is within seven's budget at Cλ (sevenC_spec). Since C λ n + 1 ≤ (λ n + 1)^C, that budget is within the budget at λ with the exponent multiplied by C (sampler_within).

theorem MIPRE.Tailored.Intro.Budget.mul_add_one_le_pow (C x : ℕ) : C * x + 1 ≤ (x + 1) ^ C

Bernoulli's inequality, on the naturals.

theorem MIPRE.Tailored.Intro.Budget.budget_pow_le (C lam n s : ℕ) : (C * lam * n + 1) ^ s ≤ (lam * n + 1) ^ (C * s)

theorem MIPRE.Tailored.Intro.Budget.sampler_within (source : Cost.Prog × Cost.Prog) {C : ℕ} (hC : 1 ≤ C) (lam n : ℕ) : (Introspection.PauliSampler.finalSampler Introspection.sevenConstant Introspection.one_le_sevenConstant ⋯ 7 (C * lam)).TimeBoundAt n ((lam * n + 1) ^ (C * Introspection.sevenC)) (C * Introspection.sevenC) ∧ (Introspection.PauliSampler.finalSampler Introspection.sevenConstant Introspection.one_le_sevenConstant ⋯ 7 (C * lam)).dim n ≤ (lam * n + 1) ^ (C * Introspection.sevenC)

The output's sampler at Cλ is within the budget at λ, with the exponent C · sevenC.