Polynomials of the output length of a polynomial-time map

A verifier, counting function or ambiguity bound for B reads a resource of size q(|f a|) on the reduced instance f a. Transporting it along a polynomial-time reduction f from A needs one polynomial P with q(|f a|) ≤ P(|a|) for every instance a of A. Turing.MultiTapeTM.ComputableInPolyTime.exists_polynomial_eval_length_le supplies it.

Main results

• Turing.MultiTapeTM.ComputableInPolyTime.exists_polynomial_eval_length_le: a polynomial of the encoded output length is bounded by a polynomial of the encoded input length.

theorem Turing.MultiTapeTM.ComputableInPolyTime.exists_polynomial_eval_length_le {α β : Type} {encIn : α ↪ List Bool} {encOut : β ↪ List Bool} {f : α → β} (hf : ComputableInPolyTime f encIn encOut) (q : Polynomial ℕ) : ∃ (P : Polynomial ℕ), ∀ (a : α), Polynomial.eval (encOut (f a)).length q ≤ Polynomial.eval (encIn a).length P

Polynomials of the output length. For a polynomial-time map f and a polynomial q, some polynomial P bounds q(|f a|) by P(|a|).