The procedure allInstancesP solves the thin matrix product on all instances (pruned data structure, $c=22$, $\theta=29/250$)

In the program programP (the programs of Section 4 with the rational parameters $c=22$, $\theta=29/250$, followed by two new procedures), procedure number $74$, allInstancesP, solves the task wanted entries of a thin matrix product on every instance, within

steps, provided the limits of the run satisfy a polynomial need $\nu(N,D,w,U)$.

The task. An instance $\mathrm{thin}(N,D,w,U,x,y,w_i,w_j,\mathit{out})$ consists of an integer matrix $X\in\mathbb Z^{N\times D}$ stored row by row at address $x$, a matrix $Y\in\mathbb Z^{D\times N}$ at $y$, with all entries of absolute value at most $U$, and $w$ distinct positions $(i_k,j_k)\in[N]\times[N]$ whose rows are stored at $w_i$ and columns at $w_j$; all of this lies below a free pointer $f$, and $N,D,U\ge1$. The procedure must write the $w$ numbers $(XY)_{i_kj_k}$ to the $w$ cells from $\mathit{out}$ and leave every other cell below $f$ unchanged.

What is proved. For every extension $\mathtt{programP}\mathbin{+\!\!+}R$ of the program, all limits, every depth $d$, every instance and memory satisfying the precondition, if the need $\nu(N,D,w,U)$ (a bound on word size, number of cells and depth, polynomial in $N,D,U$) is met by the limits at free pointer $f$ and depth $d$, then the body of allInstancesP, started on the arguments $(N,D,w,U,x,y,w_i,w_j,\mathit{out},f)$, ends within $T(N,D,w,U)$ steps in a memory satisfying the postcondition above.

The procedure first tests whether $D^{91}\le N^5$. If so, it calls the offline form of the data structure of Theorem 30 at the parameters $c=22$, $\theta=29/250$ with pruned encodings, whose time is $t_{\mathrm{off}}$; otherwise it calls the brute-force product. This is the program behind the bound $O\big(wD^{0.44274}\log D+N^2\log^2D/D^{0.07618}\big)$ of the thin regime.

Formalization Note The statement is SolvesN thinTask programP Proc.allInstancesP (allInstancesTimeP cShared30) allInstancesNeedP; $t_{\mathrm{off}}$ is tOffline32P cShared30 ratParamsP N D w and the constant of the shared stage is cShared30 $=12\,c_5+600$.