Preprocessing of the Theorem 30 data structure with pruned encodings meets its specification for all limits (preCore)

Let $P$ be a program of the light language that holds the fourteen routines of Section 4 at the numbers $40,\dots,53$, holds the body of preCore at number $54$, and meets, for every limits $\mathrm{lim}$ satisfying the standing assumptions, the specification of the shared stage with pruned encodings with constant $c$. Then for every limits $\mathrm{lim}$, preCore meets its specification:

for all parameters $p=(L,m,N)$ with $m\le L$, $t\le m$, addresses $a_X,a_Y,b_0$, matrices $X\in\mathbb Z^{N\times 4^m}$, $Y\in\mathbb Z^{4^m\times N}$ with entries of absolute value at most $U$, stored row by row at $a_X$ and $a_Y$ below $b_0$, limits satisfying $\mathrm{Lim30}(p,t,b_0,U)$, every memory $\mu$ and every depth $d$ with $d+L+6\le\mathrm{depth}$, the call $\mathrm{preCore}(L,m,t,N,4^m,a_X,a_Y,b_0)$ ends within

steps, the final memory holds the data structure for $X,Y$ at $b_0$, and it differs from $\mu$ only in the block from $b_0$ to its end. Nothing is assumed about the previous content of the block.

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.

Here $s_{\mathrm{shared}}(p)$ is the shape of the running time of the shared stage with pruned encodings, whose band term is $n_B$ times the number $\sum_{j\le m}\binom Lj9^{L-j}$ of leaves with at most $m$ nines (instead of $10^L$), and $t_{\mathrm{allTiles}}$ is the time of building the tries of all $n_B^2$ tiles.

“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.preCore]? = some preCoreBodyP → (∀ lim, Std lim → Sec2.SharedSpecP lim P c) → ∀ lim, PreCoreSpecP lim P c; the time is tPreCoreP c p t. The standing assumptions Std lim are part of Lim30.