Maintained Prefix Primal Feasibility

For all $J,M\in\mathbb N$, write $[n]=\{0,\ldots,n-1\}$, with $[0]=\varnothing$; for every instance $I$ consisting of a proof $0<M$, a load function $p:[J]\times[M]\to\mathbb R$, and proofs $0\le p(i,j)$ for every $i\in[J]$ and $j\in[M]$; and for every $k\in\mathbb N$ with $k\le J$, let $s_k$ be the state obtained by starting with weights $w(j)=1/(2M)$, assignments $a(i)=\mathrm{none}$, slacks $z(i)=0$, dual entries $y(i,j)=0$, and failure marker $\mathrm{failedAt}=\mathrm{none}$, and then recursively processing the first $k$ members of the list $0,1,\ldots,J-1$. On arrival of $i$, a state whose failure marker is already $\mathrm{some}(i')$ is left unchanged; otherwise let $E_i=\{j\in[M]\mid p(i,j)\le1\}$, and if $E_i=\varnothing$ or there exists $j\in[M]$ with $1<w(j)$, change only the failure marker to $\mathrm{some}(i)$; if neither condition holds, compute the optional machine returned by taking an argmin of $p(i,j)w(j)$ over the naturally sorted list of $E_i$, changing only the failure marker to $\mathrm{some}(i)$ if this option is $\mathrm{none}$, while if it is $\mathrm{some}(\ell)$, with $p_0=p(i,\ell)$ and $w_0=w(\ell)$, replace $w(\ell)$ by $w_0(1+p_0/2)$, $a(i)$ by $\mathrm{some}(\ell)$, $z(i)$ by $1-p_0w_0$, and $y(i,\ell)$ by $1$, leave every other coordinate unchanged, and set the failure marker to $\mathrm{none}$. The theorem assumes that the $\mathrm{failedAt}$ component of this particular state $s_k$, whose type is $\mathrm{Option}([J])$, equals $\mathrm{none}$, and asserts that all primal coordinates determined by $s_k$ are nonnegative—namely $0\le w_k(j)$ for every $j\in[M]$ and $0\le z_k(i)$ for every $i\in[J]$, including jobs with index at least $k$—and that for every $i\in[J]$ and $j\in[M]$ satisfying both $i<k$ and $p(i,j)\le1$, the covering inequality $1\le p(i,j)w_k(j)+z_k(i)$ holds; no covering inequality is quantified for an ineligible pair with $p(i,j)>1$ or for a job with $i\ge k$. When $k=0$, no arrival is processed, the failure premise holds for the initial state, the covering-inequality quantifier is empty, and only nonnegativity of all initial machine weights and all job slacks remains; when $J=0$, the hypothesis $k\le J$ forces $k=0$, all job and covering quantifiers are empty, but $M>0$ and nonnegativity of the machine weights remain; $M=0$ admits no such instance because an instance contains a proof $0<M$; and values $k>J$, or prefix states whose failure marker is not $\mathrm{none}$, do not satisfy the theorem’s hypotheses.