Cost of one layer of the dynamic program

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 $n:J\to\mathbb{N}$, with table and family lengths satisfying Poly n of degree $30000$, candidate-triple list length of degree $3$, and tables good for $M_j$ and bounded: Algorithm.TableGood says that each stored block is a valid full schedule of its set, and Algorithm.TableBounded that each stored block has all time values at most its length. The routine Uniform.layerStep, which solves the given family of sets from the table (Algorithm.solve) and records the results (Algorithm.tableOf), has running time satisfying Poly n of degree $150009$.

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