Honest histories preserve occupancy and successful row equations

For every choice of natural numbers $m,k,a,b$ satisfying $1\le k\le m$, $1\le a$, and $1\le b$, put $I=\{0,\ldots,m-1\}$ and $W=(\mathbb F_2)^a\times(\mathbb F_2)^b$, where $\mathbb F_2$ is the two-element field and addition in $W$ is componentwise addition modulo $2$. A snapshot is a function $A:I\to W\sqcup\{\bot\}$, where $\bot$ means that the cell is empty. A row $r$ consists of a subset $S_r\subseteq I$ with exactly $k$ elements, an arbitrary vector $u_r\in(\mathbb F_2)^a$, and an arbitrary vector $v_r\in(\mathbb F_2)^b$; write $\tau_r=(u_r,v_r)$. An attempt $e=(r,p,f)$ consists of such a row, either a cell $p\in I$ or no pivot $p=\bot$, and an arbitrary function $f:I\to W$. Define $F_{A,f}(i)$ to be the stored word $A(i)$ when that cell is occupied, and $f(i)$ otherwise. Define the update $T(A,e)$ as follows: if $p=\bot$, it is exactly $A$; if $p\in I$, every cell outside $S_r$ retains its previous value, every cell $i\in S_r$ with $i\ne p$ is occupied with word $F_{A,f}(i)$, and, if $p\in S_r$, cell $p$ is occupied with word $\tau_r+\sum_{j\in S_r\setminus\{p\}}F_{A,f}(j)$. Call the attempt admissible at $A$ when, in the no-pivot case, every cell of $S_r$ is already occupied, and, in the case $p\in I$, the pivot lies in $S_r$ and is empty in $A$. For every finite list of attempts $e_1,\ldots,e_n$, including $n=0$, let $A_0(i)=\bot$ for every $i\in I$, and recursively let $A_t=T(A_{t-1},e_t)$ for $1\le t\le n$. Suppose that each $e_t$ is admissible at $A_{t-1}$. Let $R$ be the list of rows from precisely those attempts whose pivot is a cell, retaining their order and any repetitions, and let $P_A(i)$ equal the stored word when $A(i)\ne\bot$ and the zero word of $W$ otherwise. Then the following three assertions hold jointly: the set $\{i\in I:A_n(i)\ne\bot\}$ is exactly $\bigcup_{r\in R}S_r$, with the union defined to be empty when $R$ is empty; for every row $r$ occurring in $R$, $\sum_{i\in S_r}P_{A_n}(i)=\tau_r$; and for every snapshot $B:I\to W\sqcup\{\bot\}$ and every attempt $e=(r,p,f)$ with these same parameters, admissibility at $B$ together with $p=\bot$ implies $T(B,e)=B$. This last quantification ranges over all snapshots and attempts, not only those in the given history, and in its no-pivot case admissibility requires that all cells in $S_r$ be occupied. All sums are finite sums in $W$, so an empty sum is the zero word; in particular, when $k=1$, the sum used to fill an admissible pivot is empty. The parameter conditions exclude zero cells, zero shares, and zero lengths for either vector component. The empty history satisfies the hypothesis, has empty occupied set and empty $R$, and makes the assertion about rows in $R$ vacuous, while retaining the universally quantified update assertion. Because $k\ge1$, an admissible first attempt in a nonempty history cannot have no pivot. There are no assumptions of disjoint row supports, randomness of the functions $f$, or additional relations among the row vectors.