Occupied-count equality certifies pairwise disjoint successful supports

For every choice of natural numbers $n,m,a,b$ satisfying $1\le m\le n$, $1\le a$, and $1\le b$, let the cells be $I=\{0,\ldots,n-1\}$, let a word be a pair in $W=(\mathbb Z/2\mathbb Z)^{\{0,\ldots,a-1\}}\times(\mathbb Z/2\mathbb Z)^{\{0,\ldots,b-1\}}$, with addition componentwise modulo two, and let a snapshot assign to each cell either no word or one word. A row $r$ consists of a subset $S_r\subseteq I$ of cardinality exactly $m$, an arbitrary vector $H_r\in(\mathbb Z/2\mathbb Z)^{\{0,\ldots,a-1\}}$, and an arbitrary vector $J_r\in(\mathbb Z/2\mathbb Z)^{\{0,\ldots,b-1\}}$. For every finite ordered list of attempts, each attempt consists of such a row $r$, either no pivot or a pivot cell $p\in I$, and an arbitrary function $F:I\to W$. Starting from the snapshot with no word at every cell, process the attempts in order as follows: an attempt with no pivot leaves the snapshot unchanged; an attempt with pivot $p$ leaves cells outside $S_r$ unchanged, assigns each cell $i\in S_r\setminus\{p\}$ its existing word if it has one and otherwise $F(i)$, and, if $p\in S_r$, assigns the pivot the word $(H_r,J_r)+\sum_{j\in S_r\setminus\{p\}}V_A(j)$, where $A$ is the snapshot immediately before this attempt and $V_A(j)$ is the word in $A$ at $j$ if present and otherwise $F(j)$; all assigned cells are occupied afterward. Assume that every attempt is admissible at its own preceding snapshot: an attempt with no pivot has every cell of its row's support already occupied, while an attempt with pivot $p$ has $p\in S_r$ and the pivot unoccupied, with no further occupancy condition on the other support cells. Retain, in their original order and with multiplicity, exactly the rows of attempts that have a pivot, and write this retained list as $(r_1,\ldots,r_k)$. Assume also that the number of occupied cells in the final snapshot is exactly $k m$. Then the retained list has pairwise disjoint supports: for every pair of positions $1\le u<v\le k$, $S_{r_u}\cap S_{r_v}=\varnothing$. There is no separate distinctness assumption on rows, supports, or attempts, and no condition relating the vectors $H_r,J_r$ or the functions $F$ across attempts. The configuration constraints exclude zero cells, zero support size, and zero lengths for either word component; support size one is allowed, in which case the pivot sum has no terms and is the zero word. The empty attempt list is included: it is admissible, its final occupied set is empty, and the cardinality equality is $0=0$; the pairwise conclusion is vacuous whenever the retained list has fewer than two entries.