Correctness of the finite FK connectivity transfer

Let $E_t=\{e_1,\dots ,e_t\}$ and let $n_0$ count vertices outside $B$ that are isolated in $G$. For each edge subset $C\subseteq E_t$, form the graph on the initially present boundary vertices and the endpoints introduced by time $t$, impose $\xi$, and retain the present edges in $C$. Let ${\pi }_t(C)$ be the resulting equivalence partition restricted to the active frontier, and let $c_t(C)$ count its equivalence classes containing no active vertex. The coefficient vector after time $t$ satisfies $W_t(\pi )=Q^{n_0}{\sum }_{\begin{array}{c}C\subseteq E_t\\ {\pi }_t(C)=\pi \end{array}}{Q}^{c_t(C)}{\prod }_{e\in C}{v}_e\mathrm{.}$ At $t=0$ the only subset is empty, every boundary vertex is active, their partition is $\xi$, and $c_0=0$. The initialized coefficient is $Q^{n_0}$, so the invariant holds.

Assume the invariant after $t-1$ edges. Introducing a new endpoint as a singleton agrees with adding that previously unseen vertex to the partial graph; a boundary endpoint is already present in the initial relation $\xi$. For each partial subset $C\subseteq E_{t-1}$, the two subsets at the next edge are exactly $C$ and $C\cup \{e_t\}$. The absent choice preserves the partition and weight; the present choice multiplies by $v_{e_t}$ and merges precisely the endpoint blocks. Thus $I+v_{e_t}{J}_{uv}$ gives the two required contributions, even when $u,v$ were already equivalent through $\xi$ or previous edges.

When vertices at their last incident edge are forgotten, no future edge is incident to them. If their block still has an active vertex, that equivalence class can connect to future edges through that vertex and is not yet closed. If removing a vertex empties its block, every boundary vertex in its $\xi$-class was already initially active and is now absent as well; no future edge can meet any member of the class. The class is therefore final, and the algorithm multiplies by $Q$ exactly once at this first emptying. This updates $c_t(C)$ and preserves the invariant. After the last edge, terminal cleanup applies the same criterion to the remaining blocks, which have no future incident edges.

For each full present-edge subset $C$, let $r_m(C)$ be the number of blocks still active just before terminal cleanup. Every equivalence class generated by $\xi$ and $C$ is counted exactly once: isolated vertices outside $B$ contribute $n_0$, classes closed earlier contribute $c_m(C)$, and the $r_m(C)$ remaining blocks each contribute one factor $Q$ in cleanup. Therefore $n_0+c_m(C)+r_m(C)=k_{\xi }(C)$, and summing the invariant from step 1.1 with these cleanup factors over $C\subseteq E$ gives the returned scalar ${\sum }_C{Q}^{k_{\xi }(C)}{v}_C=Z_{FK}^{\xi }$.

Each of the finitely many $m$ edges is processed once; every active frontier is finite and has finitely many set partitions, and terminal cleanup removes finitely many vertices. Hence the procedure terminates. For discrete $\xi$, [F3] identifies $Z_{FK}^{\xi }$ with $Z_{FK}$.