The loop of the all-edges Exact Triangle host writes the marks of all pairs (aeLoop)

Correctness and running time of the main loop aeLoop of the all-edges host of Theorem 17.

Let a program $P_0\mathbin{+\!\!+}R$ contain a solver of Lop-AE-SparseTri (procedure $p_S$ of $P_0$ solves the detection task within $T_n$ steps under the need $\nu$) and the procedures writeX, writeY, scanPairsAE and scan at their numbers. Let $X$ be the data of a run of the host (sizes $n$, $D$, prime $p$, piece size, number $m$ of instances, the hashed weights, the pieces and the query pairs of every instance) and $A$ the addresses of its arrays, and assume that the data are consistent with the bound $U$, the memory $\mu$ holds the arrays of $X$ at $A$, the arrays are laid out without overlap, the limits allow all calls (including the need of the solver at every instance), the $n^2$ cells from $f_l$ that receive the marks lie apart from everything else, and they hold $0$ initially.

Then the body of aeLoop, run at depth $d$ on its arguments, ends within

steps (with $\ell_t$ the piece size, $w_t$ the number of query pairs and $s_t$ the number of scans of instance $t$), and the final memory agrees, below the address $A.x$, with $\mu$ in which the $n^2$ cells from $f_l$ hold the marks after all $m$ instances.

Setting. The all-edges host solves All-Edges Exact Triangle: given $n\times n$ integer weight matrices $w_{AB},w_{BC},w_{AC}$ with entries of absolute value at most $U$, it writes for every pair $(a,b)$ a flag that is $1$ exactly if some $c$ has $w_{AB}(a,b)+w_{BC}(b,c)+w_{AC}(a,c)=0$. As in the proof of Theorem 17 it chooses a prime $p\le\sqrt D$, hashes the weights, splits the third part into about $4ng$ pieces of at most $\lceil s/g\rceil$ vertices ($s=\lfloor\sqrt D\rfloor$), builds one Lop-AE-SparseTri instance per piece and residue class with at most $\lfloor n^2/\sqrt D\rfloor$ query pairs, calls a detection solver on each, and scans the candidate pairs it reports, skipping pairs that are already marked. The marks are the $n^2$ flags; after the last instance they are the answer.

The number of scans of an instance counts only pairs that are not yet marked, so over the whole loop the scans are at most the false positives plus $n^2$; this is what makes the all-edges variant cost no more than the decision version.

Formalization Note The statement is Ends lim (P₀ ++ R) d (aeLoopBody pS pWriteX pWriteY pScanPairs) ⟨frame (aeLoopArgs X A fl), μ⟩ (tAELoop Tn X) (fun σ' => Kept (aeBase X fl μ X.m) σ'.mem A.x), under the hypotheses AEHostCtx, HostOk X U, HostMem X A μ, HostLay X A, HostLim lim d X U A need, AEMarksLay X A fl and the zero marks; the sum in the time is exactly tAELoop.