A query of the Theorem 30 data structure with pruned encodings meets its specification for all limits

Let $P$ be a program of the light language that holds the fourteen routines of Section 4 at the numbers $40,\dots,53$ and the body of queryAt at number $55$. Then for every limits $\mathrm{lim}$, queryAt meets its specification:

for all parameters $p=(L,m,N)$ with $m\le L$, $t\le m$, block address $b_0$, matrices $X\in\mathbb Z^{N\times4^m}$, $Y\in\mathbb Z^{4^m\times N}$ with entries of absolute value at most $U$, limits satisfying $\mathrm{Lim30}(p,t,b_0,U)$, every memory $\mu$ holding the data structure for $X,Y$ at $b_0$, all $I,J<N$ and every depth $d$ with $d+2\le\mathrm{depth}$, the call $\mathrm{queryAt}(I,J,b_0)$ ends within $t_{\mathrm{outDigits}}(L)+t_{\mathrm{queryCore}}(L,m,t)+400$ steps, returns $(XY)_{IJ}$, keeps the data structure, and changes only the $3L+m$ scratch cells from $\mathrm{WD}(b_0)$.

Setting. The data structure of Theorem 30 is built for parameters $p=(L,m,N)$ with $m\le L$ ($L$ levels, $m$ inner levels), integer matrices $X\in\mathbb Z^{N\times 4^m}$ and $Y\in\mathbb Z^{4^m\times N}$ with entries of absolute value at most $U$, and a threshold $t\le m$. It lives in a block of memory starting at an address $b_0$: the shared tables of Section 2 with the pruned encodings of the $n_B$ row bands of $X$ and column bands of $Y$ (only the leaves whose $L$ decimal digits contain at most $m$ nines are stored), the directory, the table of trie roots (one per tile) and the trie array (one trie per tile, holding the values of its boxes). The limits must satisfy the bounds $\mathrm{Lim30}$: the standing assumptions (an address fits in a word and $100\le\mathrm{word}$), the block fits in memory, and $10^m(7^LU)^2$, $7^{L+1}U$ and $10^{L+1}$ fit in a word.

Compared with the statement for a single program and limits, the hypotheses on the routines called by the query are discharged: every program holding the routines of Section 4 at their numbers meets all their specifications.

“Procedure $p$ meets its specification within $T$ steps” means: called at any depth $d$ allowed by the hypothesis, with the given argument values and a memory $\mu$ satisfying the precondition, the body of $p$ terminates within $T$ steps without violating the limits, and the returned value and final memory satisfy the postcondition.

Formalization Note The statement is Has40 P → P[Proc.queryAt]? = some queryAtBody → ∀ lim, QueryAtSpecP lim P.