Cost of one table lookup and advance step

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}$, suppose the lookup tables $\mathrm{tab}_j$ have length satisfying Poly n of degree $30000$ and contain only small blocks, and that the blocks in the marked states $u_j$ are small, where BlockSmall b means that the length of $b$ and all its time values are at most $n$. The routine Uniform.tryAdvance, which attempts Algorithm.tryAdvance from a marked state using the table, has running time satisfying Poly n of degree $60002$.

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