Cost of computing the markings for one set

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 lengths and family lengths satisfying Poly n of degree $30000$, candidate-triple list length of degree $3$, and with tables that are good for the precedence relation of $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.solveMarks, computing Algorithm.markings from Algorithm.states, has running time satisfying Poly n of degree $120009$.

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