[proofplan] The output encoding is decomposed into two contributions: the encodings of the gadgets and the wiring data between them. Since there are at most $r(|x|)$ gadgets and each gadget has length at most $q(|x|)$, the total gadget contribution is at most $r(|x|)q(|x|)$. Adding the wiring bound $s(|x|)$ gives an explicit polynomial upper bound. [/proofplan] [step:Bound the total length of the gadget encodings] Fix $x \in I$. For each index $j \in \{1,\dots,m(x)\}$, let $\ell_j(x) \in \mathbb{N}$ denote the encoding length of the gadget replacing the $j$-th local piece in the construction of $f(x)$. By hypothesis, $\ell_j(x) \le q(|x|)$ for every $j \in \{1,\dots,m(x)\}$. Therefore the total length of all gadget encodings is bounded by \begin{align*} \sum_{j=1}^{m(x)} \ell_j(x) \le \sum_{j=1}^{m(x)} q(|x|). \end{align*} Since $q(|x|)$ is independent of $j$, the right-hand side equals $m(x)q(|x|)$. Using $m(x) \le r(|x|)$ gives \begin{align*} \sum_{j=1}^{m(x)} \ell_j(x) \le r(|x|)q(|x|). \end{align*} [guided] Fix an arbitrary input $x \in I$. The construction uses $m(x)$ local pieces, so we label their replacement gadgets by the indices $j \in \{1,\dots,m(x)\}$. Define $\ell_j(x) \in \mathbb{N}$ to be the encoding length of the gadget replacing the $j$-th local piece. The hypothesis says that every local gadget has length at most $q(|x|)$. Thus, for every $j \in \{1,\dots,m(x)\}$, \begin{align*} \ell_j(x) \le q(|x|). \end{align*} Adding these $m(x)$ inequalities gives \begin{align*} \sum_{j=1}^{m(x)} \ell_j(x) \le \sum_{j=1}^{m(x)} q(|x|). \end{align*} Because $q(|x|)$ depends only on the input length and not on the gadget index $j$, the sum on the right is $m(x)q(|x|)$. Hence \begin{align*} \sum_{j=1}^{m(x)} \ell_j(x) \le m(x)q(|x|). \end{align*} Finally, the number of local pieces is polynomially bounded: $m(x) \le r(|x|)$. Multiplying this inequality by the nonnegative number $q(|x|)$ yields \begin{align*} m(x)q(|x|) \le r(|x|)q(|x|). \end{align*} Combining the two inequalities gives the desired gadget-length estimate: \begin{align*} \sum_{j=1}^{m(x)} \ell_j(x) \le r(|x|)q(|x|). \end{align*} [/guided] [/step] [step:Add the wiring data and define the polynomial bound] Let $w(x) \in \mathbb{N}$ denote the total encoding length of all wiring data between the gadgets in the construction of $f(x)$. By hypothesis, $w(x) \le s(|x|)$. Since the encoding of $f(x)$ consists only of the gadget encodings and the wiring data, we have \begin{align*} |f(x)| \le \sum_{j=1}^{m(x)} \ell_j(x) + w(x). \end{align*} Using the gadget estimate from the previous step and the wiring estimate gives \begin{align*} |f(x)| \le r(|x|)q(|x|) + s(|x|). \end{align*} Define \begin{align*} p: \mathbb{N} \to [0,\infty), \qquad p(n) = r(n)q(n) + s(n). \end{align*} The product and sum of polynomial functions are polynomial functions, so $p$ is polynomial. Therefore, for every $x \in I$, \begin{align*} |f(x)| \le p(|x|). \end{align*} This proves that the output length of the local gadget construction is bounded above by a polynomial in the input length. [/step]