Raw machine bound for deadlines not exceeding the job count

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 SmallDeadline be the type of requests whose deadline is either absent or at most the number of jobs. For $x$ in this type, let $L$ be the length of the bit encoding RequestData.bits of the request. Then the raw time bound for the compiled machine, requestRawBound x $=2000\,(\mathrm{time}+L+|\mathrm{out}|+1)$, with time the running time of Uniform.requestAnswer on the request and out the bit list Algorithm.output of the request, satisfies Poly of degree $150020$ in $L$.

Formalization Note The statement is reproduced verbatim from upstream Main.lean (openai/math, Apache-2.0, credit OpenAI). It is derived from requestRawBound_poly and gives the running-time bound used in main_theorem.