Lemma 4.6 — a deviation of agent i changes at most r − 1 of the goods allocated before i's r-th pick

Let $\succ=(\succ_1,\dots,\succ_n)$ be a profile of rankings over $m=kn$ goods, fix an agent $i$ and any ranking $\succ'_i$. For $0\le r\le k-1$ let $S_r$ and $S'_r$ be the sets of goods allocated in steps $1,\dots,rn+i-1$ of Round-Robin$(\succ)$ and of Round-Robin$(\succ'_i,\succ_{-i})$, i.e. the goods allocated right before agent $i$ receives a good in round $r+1$. Then for every $r\in[k]$,

That is, right before agent $i$'s $r$-th pick in Round-Robin$(\succ)$, at most $r-1$ goods of $S'_{r-1}$ are still unallocated: a unilateral deviation shifts only a $1/n$ fraction of the goods allocated up to any of $i$'s turns. With Lemma 4.7 it controls how the deviation redistributes goods among the other agents, and it serves both the submodular case (Theorem 4.4) and the cancelable case (Theorem 4.5).

Formalization Note The paper states the lemma for the specific deviation $\succ'_i$ of each case (Algorithm 4's output, or a strict version of $i$'s true ranking), but its proof never uses how $\succ'_i$ was chosen; the Lean statement holds for every ranking $\tau$, which contains both cases. No valuations appear. With 0-based $r$ (the paper's $r-1$), the statement reads (allocBefore σ' (r*n + i) \ allocBefore σ (r*n + i)).card ≤ r for r < k.

Formalization Note Agents are Fin n with $n\ge1$ (0-based: the paper's agent $i$ is i - 1), goods a finite type $M$ with $|M| = m$, and the paper's standing simplification $m = kn$ (p. 7) is the hypothesis hm : Fintype.card M = k * n; the paper calls it without loss of generality (dummy goods), and that reduction is not formalized. Steps of Round-Robin are 0-based: the paper's step $(r-1)n+i$ is step (r-1)*n + (i-1), and the paper's $S_r$, $S'_r$ (goods allocated in steps $1,\dots,rn+i-1$) are allocBefore σ (r*n + i) and allocBefore (Function.update σ i τ) (r*n + i) for the 0-based agent i. A ranking is a duplicate-free list of all goods; the deviating profile $(\succ'_i,\succ_{-i})$ is Function.update σ i τ.