Exact Primal Accounting Identity

For all natural numbers $\mathit{jobs}$ and $\mathit{machines}$, every instance $I$ consisting of a proof $0<\mathit{machines}$, a real load $I.\mathrm{load}(i,j)$ for every $i\in\operatorname{Fin}(\mathit{jobs})$ and $j\in\operatorname{Fin}(\mathit{machines})$, and proofs that all these loads are nonnegative, and every $k\in\mathbb N$ with $k\le \mathit{jobs}$, let $S_k$ be the state denoted by $I.\mathrm{runPrefix}(k)$, expanded as follows: start from the state $S_0$ having $S_0.\mathrm{weight}(j)=1/(2(\mathit{machines}:\mathbb R))$ for every machine, every assignment equal to $\mathrm{none}$, every slack and dual entry equal to $0$, and failure field $\mathrm{none}$; form the arrival list $\mathrm{List.ofFn}(\mathrm{id})$, whose entries are all elements of $\operatorname{Fin}(\mathit{jobs})$ in order, take its first $k$ entries, and recursively process them, retaining the next-state component of each process output (the accompanying decision is the next state’s assignment at the current arrival). For a current state $s$ and arriving job $i$, if $s.\mathrm{failedAt}=\mathrm{some}(i')$ for some $i'$, the next state is $s$ unchanged; if $s.\mathrm{failedAt}=\mathrm{none}$, put $E_i=\{j\in\operatorname{Fin}(\mathit{machines})\mid I.\mathrm{load}(i,j)\le 1\}$, and if $E_i=\varnothing$ or there exists $j$ with $1<s.\mathrm{weight}(j)$, keep every field of $s$ except set $\mathrm{failedAt}:=\mathrm{some}(i)$; otherwise, take the list obtained by sorting $E_i$ by the natural $\le$ order and apply $\operatorname{argmin}$ to $j\mapsto I.\mathrm{load}(i,j)s.\mathrm{weight}(j)$, setting only $\mathrm{failedAt}:=\mathrm{some}(i)$ if this returns no machine, while if it returns $\ell$, writing $p=I.\mathrm{load}(i,\ell)$ and $w=s.\mathrm{weight}(\ell)$, update the weight at $\ell$ to $w(1+p/2)$, the assignment at $i$ to $\mathrm{some}(\ell)$, the slack at $i$ to $1-pw$, and the dual entry $(i,\ell)$ to $1$, leave all other corresponding entries unchanged, and set the failure field to $\mathrm{none}$. Assuming the resulting state satisfies the explicit no-failure hypothesis $S_k.\mathrm{failedAt}=\mathrm{none}$, the declaration asserts that the left-hand quantity $I.\mathrm{primalObjectiveThrough}(k,S_k)$—expanded as the finite-program objective $\sum_{v\in\operatorname{Fin}(\mathit{machines})\sqcup\operatorname{Fin}(\mathit{jobs})}1\cdot X_{S_k}(v)$, where $X_{S_k}(\mathrm{inl}(j))=S_k.\mathrm{weight}(j)$ and $X_{S_k}(\mathrm{inr}(i))=S_k.\mathrm{slack}(i)$, hence exactly $\sum_{j\in\operatorname{Fin}(\mathit{machines})}S_k.\mathrm{weight}(j)+\sum_{i\in\operatorname{Fin}(\mathit{jobs})}S_k.\mathrm{slack}(i)$—is equal, in this direction, to $1+(k:\mathbb R)-\sum_{j\in\operatorname{Fin}(\mathit{machines})}S_k.\mathrm{weight}(j)$; the slack sum on the left ranges over every job, not merely indices below $k$, and all displayed quantities and the numeral $1$ in the equality are real, with $k$ explicitly coerced from $\mathbb N$ to $\mathbb R$ and $\mathit{machines}$ likewise coerced in the initial weight. The binders allow $\mathit{jobs}=0$ and $k=0$ (and $k=0$ is forced when $\mathit{jobs}=0$); then the processed prefix is empty, $S_k=S_0$, and the sum over jobs is the empty sum $0$. They do not allow $\mathit{machines}=0$, because the instance contains $0<\mathit{machines}$, so the initial division is not by zero. More generally, finite sums over empty index types have value $0$, $k$ cannot exceed the arrival-list length because of $k\le\mathit{jobs}$, and the equality is asserted only when the terminal no-failure equation is available; if that hypothesis cannot hold for particular data, there is no applicable case of the assertion for those data.