$$\begin{aligned}
\sum_{\text{such } S_i, S_j} T(S_i, S_j, S) &{\leqslant}K_1^2 \frac{{\varepsilon}}{24 K_1^2} |S|^2 \\
&= \frac{{\varepsilon}}{24} |S|^2,\end{aligned}$$ since the number of pairs $S_i, S_j$ is bounded by $K_1^2$.

Summing this over the six possible ways for a triple to be bad completes the proof of Lemma \[lem:ignore\_bad\_triples\].

In view of Lemmas \[lem:ignore\_S0\] and \[lem:ignore\_bad\_triples\], it remains to show that the number of solutions among the good triples is at most $\left(\frac{1}{12} + \frac{{\varepsilon}}{4}\right)|S|^2$, for a suitable choice of the coefficients $a_1, a_2 {\text{ and }}a_3$. The values we will choose are $a_1 = 1, a_2 = M {\text{ and }}a_3 = M+1$, where $$\label{eqn:condition_on_M}
M > \left(\frac{1000 K_1^4K_2^2}{{\varepsilon}^2}\right)^{K_1}.$$

We can now prove the following lemma:

\[lem:no\_bad\_cycles\] With the values of $a_1, a_2 {\text{ and }}a_3$ that we have chosen, the product of the labels along any cycle in $G$ must be 1.

This immediately tells us that $G$ has no loops (edges from a vertex to itself). In view of the fact that an edge from $S_i$ to $S_j$ with label $x$ is accompanied by an edge from $S_j$ to $S_i$ with label $x^{-1}$, this also tells us that there can be at most one edge from $S_i$ to $S_j$.

We 