Unrelated-Machines Load-Balancing Model and Algorithm

Instance. For explicit natural numbers $\mathit{jobs}=n$ and $\mathit{machines}=m$, an Instance n m consists of a proof that $0<m$, a total function $p:\operatorname{Fin}(n)\to\operatorname{Fin}(m)\to\mathbb R$, and a proof that $0\le p_{ij}$ for every job $i$ and machine $j$. Thus $n$ may be zero, in which case the load function and its nonnegativity condition have empty job domain; an inhabitant cannot exist when $m=0$ because it would contain a proof of $0<0$. No upper bound on a load is included.

eligible. For implicit natural numbers $n,m$, an instance $I$ with $0<m$ and nonnegative total load function $p_{ij}$, and a job $i\in\operatorname{Fin}(n)$, eligible I i is the finite set $E_i=\{j\in\operatorname{Fin}(m)\mid p_{ij}\le1\}$. Because the instance separately guarantees $p_{ij}\ge0$, these are exactly the machines with $0\le p_{ij}\le1$; the set may be empty despite $m>0$. If $n=0$, there is no value of $i$ at which to evaluate this function.

mem_eligible_iff. For implicit natural numbers $n,m$, every instance $I$ with $0<m$ and nonnegative loads, every $i\in\operatorname{Fin}(n)$, and every $j\in\operatorname{Fin}(m)$, the theorem asserts the exact equivalence $j\in I.\mathrm{eligible}(i)\iff p_{ij}\le1$, with no additional hypothesis. An instantiation has no possible job argument when $n=0$, and no instance exists when $m=0$.

EligiblePair. For implicit natural numbers $n,m$ and an instance $I$, I.EligiblePair is the subtype of pairs $(i,j)\in\operatorname{Fin}(n)\times\operatorname{Fin}(m)$ equipped with a proof that $j\in I.\mathrm{eligible}(i)$, equivalently a proof that $p_{ij}\le1$. The type is empty when $n=0$ and may also be empty when every job-machine load exceeds $1$; the instance itself forces $m>0$.

EligiblePairThrough. For implicit natural numbers $n,m$, an instance $I$, and any natural number $k$, I.EligiblePairThrough k is the subtype of eligible pairs $(i,j)$ additionally equipped with the condition that the natural value of $i$ is less than $k$. It is empty for $k=0$ or $n=0$; if $k\ge n$, it contains every eligible pair, and values of $k$ beyond $n$ introduce no extra jobs because job indices remain in $\operatorname{Fin}(n)$.

PrimalVar. For explicit natural numbers $n,m$, PrimalVar n m is the disjoint sum $\operatorname{Fin}(m)\sqcup\operatorname{Fin}(n)$: every value is either a machine-tagged index or a job-tagged index. This declaration has no positivity assumption; if $m=0$ the machine side is empty, if $n=0$ the job side is empty, and if both are zero the whole type is empty.

lp. For implicit natural numbers $n,m$ and an instance $I$ with loads $p_{ij}\ge0$ and $m>0$, I.lp is finite primal-dual data whose primal-coordinate type is $\operatorname{Fin}(m)\sqcup\operatorname{Fin}(n)$ and whose constraint/dual-coordinate type is the eligible pairs $E=\{(i,j)\mid p_{ij}\le1\}$. For a constraint $q=(i,j)\in E$, the coefficient of a machine coordinate $j'$ is $p_{ij'}$ when $j'=j$ and $0$ otherwise, while the coefficient of a job coordinate $i'$ is $1$ when $i'=i$ and $0$ otherwise; every right-hand side and every cost is $1$. Under the imported finite-LP operations, this yields primal objective $\sum_jx_j+\sum_i z_i$, primal constraint $p_{ij}x_j+z_i\ge1$ for each $(i,j)\in E$, dual objective $\sum_{(i,j)\in E}y_{ij}$, machine constraint $\sum_{i:(i,j)\in E}p_{ij}y_{ij}\le1$, and job constraint $\sum_{j:(i,j)\in E}y_{ij}\le1$ when the corresponding feasibility predicates are invoked; the declaration itself supplies the coefficients, right sides, and costs rather than asserting feasibility. If $n=0$, or if there are no eligible pairs, the constraint and dual-variable type is empty, while the $m$ machine coordinates and their unit costs remain.

lp_isCoveringPacking. For implicit natural numbers $n,m$ and every instance $I$, the theorem supplies the imported IsCoveringPacking proposition for I.lp: for every primal coordinate $v$ and eligible constraint $q$, its coefficient is nonnegative; every eligible constraint has nonnegative right-hand side; and every primal coordinate has nonnegative cost. Concretely, the coefficients are either a nonnegative load $p_{ij}$, $1$, or $0$, and all right sides and costs are $1$. If the eligible-pair type is empty, the coefficient and right-side assertions are vacuous; if $n=0$, the remaining machine-coordinate cost assertions still say $0\le1$. It asserts no feasibility, optimality, or duality conclusion.

lpThrough. For implicit natural numbers $n,m$, an instance $I$, and any $k\in\mathbb N$, I.lpThrough k has all machine and all job primal coordinates $\operatorname{Fin}(m)\sqcup\operatorname{Fin}(n)$ but only constraints $(i,j)$ satisfying both $p_{ij}\le1$ and $i<k$. At such a constraint, a machine coordinate $j'$ has coefficient $p_{ij'}$ if $j'=j$ and $0$ otherwise, a job coordinate $i'$ has coefficient $1$ if $i'=i$ and $0$ otherwise, and every right-hand side and every cost is $1$. Hence its primal constraints are $p_{ij}x_j+z_i\ge1$ only for eligible pairs with $i<k$, while its objective still includes every machine coordinate and every job coordinate. For $k=0$ there are no constraints; for $k\ge n$ this has all eligible constraints; $k>n$ is silently truncated by the finite job type, and $n=0$ gives no constraints.

lpThrough_isCoveringPacking. For implicit natural numbers $n,m$, every instance $I$, and every unrestricted $k\in\mathbb N$, the theorem asserts that every coefficient, right-hand side, and cost in I.lpThrough k is nonnegative. The coefficients are precisely nonnegative loads, $1$, or $0$, and every right side and cost is $1$. When $k=0$, $n=0$, or the relevant jobs have no eligible pairs, the coefficient and right-side portions may be vacuous, while nonnegativity of the costs of all machine and job coordinates remains; no feasibility or optimization assertion is included.

State. For explicit natural numbers $n,m$, a State n m contains total functions $\mathrm{weight}:\operatorname{Fin}(m)\to\mathbb R$, $\mathrm{assignment}:\operatorname{Fin}(n)\to\operatorname{Option}(\operatorname{Fin}(m))$, $\mathrm{slack}:\operatorname{Fin}(n)\to\mathbb R$, and $\mathrm{dual}:\operatorname{Fin}(n)\to\operatorname{Fin}(m)\to\mathbb R$, together with $\mathrm{failedAt}\in\operatorname{Option}(\operatorname{Fin}(n))$. No invariant requires weights, slacks, or dual values to be nonnegative, assignments to be eligible, or failedAt to be the first failure. The functions also have values for every unprocessed index whenever their domains are nonempty. If $n=0$, all job-indexed functions have empty domain and failedAt can only be none; if $m=0$, weights and each dual row have empty domain and every assignment must be none.

initialState. For implicit natural numbers $n,m$ and an explicit instance argument $I$—whose load data are unused but whose field proves $m>0$—I.initialState assigns every machine weight the value $1/(2m)$, every job assignment none, every job slack $0$, every job-machine dual entry $0$, and failedAt = none. Real division is a total operation, and here the denominator is nonzero because $m>0$. If $n=0$, the assignment, slack, and dual clauses are functions on an empty job domain.

noEligibleMachine. For implicit natural numbers $n,m$, an instance $I$, and a job $i\in\operatorname{Fin}(n)$, I.noEligibleMachine i is the proposition that $\{j\mid p_{ij}\le1\}=\varnothing$, equivalently that no machine has load at most $1$ for job $i$. The instance guarantees $m>0$, so this can hold even though machines exist. If $n=0$, there is no job argument at which the predicate can be formed.

hasOverweightMachine. For implicit natural numbers $n,m$, an instance argument $I$ and an arbitrary state $s$, I.hasOverweightMachine s is the proposition $\exists j\in\operatorname{Fin}(m),\ 1<s.\mathrm{weight}(j)$. The load, assignments, slack, dual array, and failure marker are ignored; the instance argument contributes only its indexing and the fact $m>0$. No reachability or nonnegativity assumption is imposed on $s$.

failureCondition. For implicit natural numbers $n,m$, an instance $I$, arbitrary state $s$, and job $i\in\operatorname{Fin}(n)$, I.failureCondition s i is exactly the inclusive disjunction that either no $j$ satisfies $p_{ij}\le1$, or there exists a machine $j$ with $s.\mathrm{weight}(j)>1$. It does not inspect s.failedAt, assignments, slacks, or dual values and adds no other failure case.

chooseMachine. For implicit natural numbers $n,m$, an instance $I$, arbitrary state $s$, and job $i$, I.chooseMachine s i sorts the finite eligible set $\{j\mid p_{ij}\le1\}$ by the natural order on $\operatorname{Fin}(m)$ and applies list argmin to the real-valued score $j\mapsto p_{ij}s.\mathrm{weight}(j)$. It returns none when the eligible list is empty and otherwise returns the deterministic element selected as a minimum from that ordered list; ties require no uniqueness and are resolved by the library operation on the sorted list. The definition does not inspect failedAt and assumes no sign condition on the arbitrary state's weights.

IsMinimumChoice. For implicit natural numbers $n,m$, an instance $I$, arbitrary state $s$, job $i$, and machine $j$, I.IsMinimumChoice s i j is the conjunction $p_{ij}\le1$ and, for every machine $k$, the implication $p_{ik}\le1\Rightarrow p_{ij}s.\mathrm{weight}(j)\le p_{ik}s.\mathrm{weight}(k)$. It asserts eligibility and weak minimality only; it does not assert uniqueness, a particular tie-breaking outcome, absence of failure, or that $j$ was actually returned by chooseMachine.

chooseMachine_spec. For implicit natural numbers $n,m$, every instance $I$, every implicit arbitrary state $s$, job $i$, and machine $j$, and the hypothesis I.chooseMachine s i = some j, the theorem concludes that $p_{ij}\le1$ and that $p_{ij}s.\mathrm{weight}(j)\le p_{ik}s.\mathrm{weight}(k)$ for every $k$ with $p_{ik}\le1$. If the eligible set is empty, the hypothesis cannot hold. The theorem has no assumption about s.failedAt, reachability, weight signs, uniqueness, or tie order, and it asserts only this one implication.

step. For implicit natural numbers $n,m$, an instance $I$, any state $s$, and any job $i$, I.step s i is a total deterministic state transition with these exact branches. If s.failedAt = some f for any job $f$, it returns $s$ unchanged without testing $i$. If s.failedAt = none and either $i$ has no machine with $p_{ij}\le1$ or some current weight exceeds $1$, it changes only failedAt to some i. Otherwise it invokes chooseMachine; if that unexpectedly returns none, it again changes only failedAt to some i. If it returns some ell, writing $p=p_{i\ell}$ and $w=s.\mathrm{weight}(\ell)$, the result changes only machine $\ell$'s weight to $w(1+p/2)$, job $i$'s assignment to some ell, job $i$'s slack to $1-pw$, and dual entry $(i,\ell)$ to $1$, preserves every other weight, assignment, slack, and dual entry—including all other entries in row $i$—and sets failedAt to none. Because the input state and arrival are arbitrary, repeated or out-of-order calls can overwrite the named assignment and slack, and no invariant on prior state values is assumed; when $n=0$ there is no job value with which to call the transition.

process. For implicit natural numbers $n,m$ and an instance $I$, I.process is an online-process record with request type $\operatorname{Fin}(n)$, state type State n m, and decision type $\operatorname{Option}(\operatorname{Fin}(m))$. Its designated initial state is I.initialState; on any current state $s$ and request $i$, it computes $s'=I.\mathrm{step}(s,i)$ and returns the pair $(s',s'.\mathrm{assignment}(i))$. Thus the emitted decision is the post-transition assignment entry, even on a failure or already-failed arbitrary state, so it is not definitionally forced to be none if that state already stored some j. The step is total for every state and valid request and can be fed repeated or out-of-order request lists; if $n=0$, the request type has no values.

arrivals. For implicit natural numbers $n,m$ and an explicit instance argument $I$ that is otherwise unused, I.arrivals is List.ofFn id, namely the length-$n$ list of all elements of $\operatorname{Fin}(n)$ in order $0,1,\ldots,n-1$. It is empty when $n=0$; the instance guarantees $m>0$ but neither its loads nor its machines affect the list.

runPrefix. For implicit natural numbers $n,m$, an instance $I$, and any $k\in\mathbb N$, I.runPrefix k starts at I.initialState and processes, from left to right, the first $k$ entries of the list $0,1,\ldots,n-1$, retaining the state component of each I.process transition. Because list take truncates, exactly the first $\min(k,n)$ arrivals are used: $k=0$ returns the initial state, and every $k\ge n$ processes the whole list. If a transition records a failure, every subsequent transition returns that state unchanged because failure is absorbing. When $n=0$, every prefix is the initial state.

finalState. For implicit natural numbers $n,m$ and an instance $I$, I.finalState is I.runPrefix n, hence the state obtained from the designated initial state after processing the entire list $0,1,\ldots,n-1$. If a job records a failure, this is the unchanged absorbing state from that first failure onward; if $n=0$, it is exactly the initial state.

Succeeded. For implicit natural numbers $n,m$ and an instance $I$, I.Succeeded is solely the proposition I.finalState.failedAt = none. It adds no explicit claim about assignments, eligibility, primal or dual feasibility, weights, or loads. When $n=0$, the final state is initial and this equality holds.

AssignsAll. For implicit natural numbers $n,m$ and an instance $I$, I.AssignsAll is the proposition that for every $i\in\operatorname{Fin}(n)$ there exists a $j\in\operatorname{Fin}(m)$ such that I.finalState.assignment i = some j. It does not separately require Succeeded, eligibility of the stored machine, or any load bound. The assertion is vacuously true when $n=0$; an instance always has $m>0$.

stateAssignedLoad. For implicit natural numbers $n,m$, an instance $I$, an arbitrary state $s$, and a machine $j$, I.stateAssignedLoad s j is the finite sum $\sum_{i\in\operatorname{Fin}(n)}\bigl(\text{if }s.\mathrm{assignment}(i)=\mathrm{some}(j)\text{ then }p_{ij}\text{ else }0\bigr)$. It ignores weights, slacks, dual values, and failedAt, and it neither requires $s$ to be reachable nor checks that stored assignments are eligible. The empty-job sum is $0$.

assignedLoadThrough. For implicit natural numbers $n,m$, an instance $I$, any $k\in\mathbb N$, and a machine $j$, I.assignedLoadThrough k j is $\sum_i\bigl(\text{if }(I.\mathrm{runPrefix}(k)).\mathrm{assignment}(i)=\mathrm{some}(j)\text{ then }p_{ij}\text{ else }0\bigr)$, where runPrefix k processes only the first $\min(k,n)$ canonical arrivals and freezes at any earlier failure. The sum itself ranges over all jobs, including indices not below $k$, and relies on the stored state values to select terms. It is $0$ for $k=0$ and for $n=0$, and for every $k\ge n$ it uses the final state.

assignedLoad. For implicit natural numbers $n,m$, an instance $I$, and a machine $j$, I.assignedLoad j is $\sum_i\bigl(\text{if }I.\mathrm{finalState}.\mathrm{assignment}(i)=\mathrm{some}(j)\text{ then }p_{ij}\text{ else }0\bigr)$. If the canonical run fails, assignments stored before the absorbing failure still contribute and unassigned jobs do not; no success or eligibility premise is imposed. The value is $0$ when $n=0$.

primalVector. For implicit natural numbers $n,m$, an explicit instance argument $I$ whose data are otherwise unused, and any state $s$, I.primalVector s is the total real vector on $\operatorname{Fin}(m)\sqcup\operatorname{Fin}(n)$ that sends a machine-tagged coordinate $j$ to $s.\mathrm{weight}(j)$ and a job-tagged coordinate $i$ to $s.\mathrm{slack}(i)$. Assignments, dual entries, and failedAt are discarded, and no nonnegativity or reachability property is asserted. If $n=0$, there are no job-tagged coordinates.

algorithmDualVector. For implicit natural numbers $n,m$, an instance $I$, and any state $s$, I.algorithmDualVector s is the total real function on eligible pairs: at an eligible pair $q=(i,j)$, including its proof that $p_{ij}\le1$, it returns the rectangular-array entry $s.\mathrm{dual}(i,j)$. The eligibility proof does not affect the value, ineligible array entries are absent from the output domain rather than set to zero, and no sign, feasibility, assignment, or reachability condition is imposed. The domain is empty when $n=0$ or when no pair is eligible.

restrictDual. For implicit natural numbers $n,m$, an instance $I$, any full function $y$ from eligible pairs to $\mathbb R$, and any $k\in\mathbb N$, I.restrictDual y k is the function on eligible pairs $(i,j)$ with $i<k$ that returns exactly $y(i,j)$ after forgetting the additional prefix proof. It changes no values and imposes no feasibility condition. Its domain is empty for $k=0$; for $k\ge n$ it contains every eligible pair, and $n=0$ makes both domains empty.

jobDualMass. For implicit natural numbers $n,m$, an instance $I$, any real function $y$ on eligible pairs, and a job $i$, I.jobDualMass y i is the sum over every eligible pair $q=(i',j)$ of $y(q)$ when $i'=i$ and $0$ otherwise, equivalently $\sum_{j:p_{ij}\le1}y_{ij}$. No nonnegativity or feasibility assumption is made. If job $i$ has no eligible machine, the value is the empty sum $0$; if $n=0$, there is no job argument.

DualAssignsAll. For implicit natural numbers $n,m$, an instance $I$, and a real function $y$ on eligible pairs $E=\{(i,j)\mid p_{ij}\le1\}$, I.DualAssignsAll y is the conjunction of the fully expanded conditions: $y_{ij}\ge0$ for every $(i,j)\in E$; $\sum_{i:(i,j)\in E}p_{ij}y_{ij}\le1$ for every machine $j$; $\sum_{j:(i,j)\in E}y_{ij}\le1$ for every job $i$; and, additionally, $\sum_{j:(i,j)\in E}y_{ij}=1$ for every job $i$. There are no values for ineligible pairs. If any existing job has no eligible machine, its required equality is the impossible equation $0=1$; if $n=0$, the eligible domain and all job conditions are empty, while every machine condition is $0\le1$, so the predicate holds for the unique empty-domain function.

PrimalFeasibleThrough. For implicit natural numbers $n,m$, an instance $I$, any $k\in\mathbb N$, and any state $s$, I.PrimalFeasibleThrough k s is exactly the conjunction that $s.\mathrm{weight}(j)\ge0$ for every machine $j$, $s.\mathrm{slack}(i)\ge0$ for every job $i$, and $1\le p_{ij}s.\mathrm{weight}(j)+s.\mathrm{slack}(i)$ for every pair with $p_{ij}\le1$ and $i<k$. All job slacks, including those whose indices are not below $k$, are subject to nonnegativity, while only prefix eligible pairs generate covering constraints; assignments, dual entries, and failure status are ignored. For $k=0$ the covering constraints are vacuous but coordinate nonnegativity remains; for $k\ge n$ all eligible constraints are included, and when $n=0$ only machine-weight nonnegativity remains.

primalObjectiveThrough. For implicit natural numbers $n,m$, an instance $I$, any $k\in\mathbb N$, and any state $s$, I.primalObjectiveThrough k s is the imported finite-LP objective $\sum_j s.\mathrm{weight}(j)+\sum_i s.\mathrm{slack}(i)$ because every machine and job coordinate has unit cost. Despite the parameter $k$, the value includes every job slack and is definitionally independent of which prefix constraints exist; no feasibility, nonnegativity, reachability, or success assumption is imposed. For $n=0$ the job sum is $0$, and the same objective is used even at $k=0$ or $k>n$.

logarithmicLoadBound. For implicit natural numbers $n,m$ and an explicit instance argument $I$ whose loads and job count are unused, I.logarithmicLoadBound is the exact real number $\log(3m)/\log(3/2)$, with $m$ coerced from $\mathbb N$ to $\mathbb R$. The instance guarantees $m>0$, so $3m>0$, and $\log(3/2)>0$ is nonzero; real logarithm and division are total operations in any case. The value has no rounding, ceiling, asymptotic qualification, or dependence on $n$, so $n=0$ leaves it unchanged.