Worst-case bound on the run time of the all-edges host at the middle dimension after the choice of the prime

Let $x$ be an Exact Triangle instance with $n$ vertices per part and weight bound $U$ satisfying the precondition of the host in a memory $\mu$ with free pointer $f$, let $16\le D\le n$ and $1\le g\le\lfloor\sqrt D\rfloor$, and let $T_n$ be any time function of the Lop-AE-SparseTri solver. Write $s=\lfloor\sqrt D\rfloor$, $q=\lceil s/g\rceil$ and $D_{\mathrm m}=qs$. Then the time of the run after the choice of the prime, for the host data with inner dimension $D_{\mathrm m}$, is bounded by an expression that no longer depends on the prime or on the instance data:

where the loop bound is

Here $\sup T_n(n,D_{\mathrm m},w)$ is the largest time of the solver on $n$ vertices, inner dimension $D_{\mathrm m}$ and at most $w$ query pairs, and $F(n,U,D)=\lfloor c_F\,\kappa(n,U)\,n^3\log n/\sqrt D\rfloor$ is the bound on the false positives of the hashing (with $\kappa(n,U)=\max(1,\log U/\log n)$ and $c_F$ the constant of the hashing lemma).

The bound uses that the prime is at most $\sqrt D$, that there are at most $4ng$ instances and chunks, that each instance has inner dimension $D_{\mathrm m}\le D$ and at most $\lfloor n^2/\sqrt D\rfloor$ query pairs, and that the scans are at most the false positives plus the $n^2$ pairs (each pair is scanned to success at most once). It is the step from the time of one run to the bound of Theorem 17 at the middle dimension.

Formalization Note The statement is aeRunTime Tn (midHostData x D g) x.U ≤ tDblTable (bitLen x.U) + 3 * tResidues (x.n * x.n) (bitLen x.U) + tClasses x.n (Nat.sqrt D) + tChunks (Nat.sqrt D) (4 * x.n * g) + midLoopBound Tn x.n x.U D g + 80, under x.Pre μ fr and BigCase x.n D g; all quantities are natural numbers.