The (min,+)-product in time $O(T(n,36u)\log^2 u)$ from all-edges Exact Triangle in time $T$

Let $T(n,u)$ be a time in which All-Edges Exact Triangle is solved (on $n$ vertices per part with weights of absolute value at most $u$), with $T(n,u)\ge n^2$ for $n\ge1$. Then there is a constant $C\ge0$ such that the $(\min,+)$-product of $n\times n$ integer matrices with entries of absolute value at most $u$ is solved in time

The problems. All-Edges Exact Triangle: given $w_{AB},w_{BC},w_{AC}\in\mathbb Z^{n\times n}$, output for every pair $(a,b)$ whether some $c$ has $w_{AB}(a,b)+w_{BC}(b,c)+w_{AC}(a,c)=0$. The $(\min,+)$-product: given $A,B\in\mathbb Z^{n\times n}$ stored in memory, write $C_{ij}=\min_k(A_{ik}+B_{kj})$ to the output area, changing no other cell below the free pointer. "Solved in time $T$" refers to programs of the library's light language, which compiles to the word RAM: one program, with a polynomially bounded need, solves every instance with $n\ge1$ and bound $1\le U\le u$ within $T(n,u)$ steps.

The reduction goes through the all-pairs problem: for every pair $(i,j)$ decide whether some $k$ has $A_{ik}+B_{kj}<V_{ij}$ for a threshold matrix $V$. Each such question reduces to all-edges Exact Triangle over the binary prefixes of the weights (with weights scaled by $6$), and the $(\min,+)$-product follows by binary search on every entry with $O(\log u)$ all-pairs calls. This is Theorem 21(b) of Alman and Vassilevska Williams with the decision problem replaced by its all-edges version, so that no factor $n^{1/3}$ is lost.

Formalization Note The statement is SolvedIn aeTask T → (∀ n u, 1 ≤ n → (n:ℝ)^2 ≤ T n u) → ∃ C ≥ 0, SolvedIn mpTask (fun n u => C * (6000 * (T n (6 * (6 * u)) * logU (6 * u)) * logU u)), with logU v = log (max v 2).