Cost of computing the output from a closed precedence matrix

Throughout, a routine R : Uniform f is a program in the compiler's while-language Code, with a charge function, that computes the function family $f_i$ on encoded data. R.time i x is the charge of $R$ on the encoding of $x$, a natural number that bounds the number of evaluation steps of the program on that input. For $s,f:I\to\mathbb{N}$, the predicate Poly s f d means that there is a constant $C$ with $f(i)\le C\,(s(i)+2)^d$ for all $i\in I$. Let $J$ be an index type with $s,n:J\to\mathbb{N}$ where $n$ satisfies Poly s of degree $1$, and let $d_j$ be optional deadlines whose value (default $0$) satisfies Poly s of degree $1$. The routine Uniform.answerMatrix, returning answerMatrix M d, namely a schedule for the deadline when $d$ is given and otherwise an optimal one, has running time satisfying Poly s of degree $150011$.

Formalization Note The statement is reproduced verbatim from upstream RequestBounds.lean (openai/math, Apache-2.0, credit OpenAI). It feeds the bound requestRawBound_poly and the running-time statement of main_theorem.