Lemma 7 ([Pinning by vertex and pair scores]). Let F=(P Q,L) be a finite bipartite graph for which color refinement, starting with the two part colors, becomes discrete within each part. There are real vertex scores s_t , t∈P Q , and pair …

Let ℓ_0 be the two part colors and, at round t , let h_t(u) be the histogram of ℓ_ t-1 -colors among the neighbors of u . The new color is ℓ_t(u)=(ℓ_ t-1 (u),h_t(u)) . Choose R≥1 rounds giving a discrete coloring. At round t assign the vertex score -\|h_t(a)\|^2 to type a and the pair score 2h_t(a)(ℓ_ t-1 (b))+2h_t(b)(ℓ_ t-1 (a)) to every (a,b)∈P×Q , including nonedges. The total round score of f is F_t(f)=-∑_u\|h_t(f(u))\|^2 +2∑_u∑_ v∈N_F(u) h_t(f(u))(ℓ_ t-1 (f(v))). Here N_F(u) is the neighbor set of u . Both sums are indexed by the vertices and directed incidences of the source graph F , even when f repeats a type. If ℓ_ t-1 (f(u))=ℓ_ t-1 (u) for every u , the inner neighbor sum equals ⟨h_t(f(u)),h_t(u)⟩ . Thus F_t(f) , =∑_u(2⟨h_t(f(u)),h_t(u)⟩ -\|h_t(f(u))\|^2); , =∑_u\|h_t(u)\|^2 -∑_u\|h_t(f(u))-h_t(u)\|^2. The first equality uses only preservation of previous colors. It therefore applies to noninjective maps and to maps taking edges to nonedges. In this situation F_t(id)-F_t(f) is a nonnegative integer, zero precisely when f also preserves all new colors. To combine the rounds into a single score, set M=_ f,\,1≤t≤R |F_t(f)-F_t(id)|, L_0=M+2, Q(f)=∑_ t=1 ^R L_0^ R-t F_t(f). The maximum defining M is finite. For a nonidentity map, let t be the first round at which a color fails to be preserved. All earlier scores tie the identity; the loss at round t is at least L_0^ R-t . Its possible later advantage is at most M∑_ j=0 ^ R-t-1 L_0^j<L_0^ R-t . Hence its total score is strictly smaller. A nonidentity map must have such a first round because the final colors are discrete. The weighted sums of the round vertex scores and pair scores are the required s_t,s_ ab . Finiteness of the set of maps gives the positive gap.