The all-edges Exact Triangle host at the middle dimension, assembled as a solver from a Lop-AE-SparseTri solver

Let $P_0$ be a program of the light language in which procedure $p_S$ solves Lop-AE-SparseTri (Definition 13 of Alman and Vassilevska Williams, the detection version) within the time $T_n(n,D,w)$ under the need $\nu$, and in which the procedures $p_D$ and $p_G$ compute the parameter functions $D(n)$ and $G(D)$: called on $x\ge1$, $p_D$ returns $D(x)$ within $t_D(x)$ steps, changes no cell and forms only numbers up to $w_D(x)$, and likewise $p_G$ with $G,t_G,w_G$, in every extension of $P_0$. Assume $D(n)\ge1$ for $n\ge1$.

Append to $P_0$ the $34$ procedures of the all-edges host at the middle dimension, $\mathtt{midProcs}(p_S,p_D,p_G,|P_0|)$. Then procedure number $|P_0|+33$ of the resulting program solves All-Edges Exact Triangle within the time

under the need $\nu_{\mathrm{mid}}(n,U)$, and so does it in every extension of the program. Here All-Edges Exact Triangle on $n$ vertices per part with weight bound $U$ asks, given $w_{AB},w_{BC},w_{AC}\in\mathbb Z^{n\times n}$ stored in memory, to write to the $n^2$ output cells the flag of every pair $(a,b)$, which is $1$ exactly if some $c$ has $w_{AB}(a,b)+w_{BC}(b,c)+w_{AC}(a,c)=0$, changing no other cell below the free pointer.

The core time $t_{\mathrm{core}}(n,U)$ is the time of computing $D=D(n)$, $g=G(D)$ and the tests, plus either the brute force (if $D<16$, $n<D$, $g<1$ or $g>\lfloor\sqrt D\rfloor$) or the reduction of Theorem 17: the choice of the prime, the residues, classes and chunks, and at most $4ng$ calls of the solver at the middle dimension $D_{\mathrm m}=\lceil s/g\rceil\cdot s$ ($s=\lfloor\sqrt D\rfloor$) with at most $\lfloor n^2/\sqrt D\rfloor$ query pairs each, plus the scans. The need $\nu_{\mathrm{mid}}$ adds to the need of the host of Theorem 17 the need of the solver at the middle dimension, and room for the $n^2$ flags.

"Procedure $p$ solves the task within $T$ under the need $\nu$" means: for every extension of the program, all limits, every depth and every instance in memory satisfying the task's precondition, if the limits meet $\nu(\text{size},\text{bound})$, the body of $p$ ends within $T(\text{size},\text{bound})$ steps in a state satisfying the task's postcondition.

Formalization Note The statement is Solves aeTask (P₀ ++ midProcs pS pD pG P₀.length) (P₀.length + 33) (midHostTime Dfun Gfun tD tG Tn) (midHostNeed Dfun Gfun wD wG need) under SolvesN lopDetectTask P₀ pS Tn need, ∀ R, ParamProc (P₀ ++ R) pD Dfun tD wD, ∀ R, ParamProc (P₀ ++ R) pG Gfun tG wG and ∀ n, 1 ≤ n → 1 ≤ Dfun n.