The shared stage with pruned encodings meets its specification in every program beginning with base58

Let $R$ be any list of procedures and $\mathrm{lim}$ limits satisfying the standing assumptions (an address fits in a word, and $100\le\mathrm{word}$). In the program $\mathtt{base58}\mathbin{+\!\!+}R$, the procedure sharedP (number $31$) meets the specification of the shared stage with pruned encodings with the constant $c_{30}=12\,c_5+600$:

for all parameters $p=(L,m,N)$ with $m\le L$, addresses $a_X,a_Y,b_0$, matrices $X\in\mathbb Z^{N\times4^m}$, $Y\in\mathbb Z^{4^m\times N}$, a bound $V$, and every memory $\mu$ satisfying the precondition of the shared stage (the matrices stored at $a_X,a_Y$ with entries of absolute value at most $V$, the block from $b_0$ in memory, and the needed numbers fitting in a word), and every depth $d$ with $d+L+3\le\mathrm{depth}$, the call $\mathrm{sharedP}(L,m,N,4^m,a_X,a_Y,b_0)$ ends within $c_{30}\cdot s_{\mathrm{shared}}(p)$ steps, leaves behind the shared tables, the directory, and for every band $\beta<n_B$ the encodings of the row band of $X$ and the column band of $Y$ at the leaves whose $L$ decimal digits contain at most $m$ nines, and changes nothing outside the shared part of the block.

The time shape is

where $K=\binom Lm$, $K_0=\lfloor\sqrt K\rfloor$, $b(p)$ is the cost of laying out one band, and $r(L,m)=\sum_{j\le m}\binom Lj9^{L-j}$ is the number of strings of $L$ decimal digits with at most $m$ nines. The pruned encoder only visits these strings, which replaces the term $10^L$ per band of the unpruned shared stage.

base58 is the list of procedures $0$-$57$: the program of Section 2 for the thin matrix product, the pruned shared stage ($29$-$31$), eight unused slots, the routines of Section 4 ($40$-$53$) and the four routines that know the memory map ($54$-$57$). It is the common beginning of the programs for Theorem 30, Corollaries 26, 31 and 32 and the pruned all-instances program.

“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 Sec2.SharedSpecP lim (base58P ++ R) cShared30 (the Section 4 program list is named base58P in the uploaded bundles).