Lemma 4.7 — every agent gets at most 2(r − 1) goods of S′_{r−1} ∖ S′_0 in Round-Robin(≻)

In the setting of Lemma 4.6 — a profile of rankings $\succ$ over $m=kn$ goods, an agent $i$, any ranking $\succ'_i$, and the sets $S'_r$ of goods allocated in steps $1,\dots,rn+i-1$ of Round-Robin$(\succ'_i,\succ_{-i})$ — let $(A_1,\dots,A_n)$ be the allocation returned by Round-Robin$(\succ)$. Then for every $r\in[k]$ and every agent $j$,

No agent accumulates in the equilibrium allocation more than twice its fair share of the goods that the deviation run allocates between $i$'s first and $r$-th turns. This is the bound that makes the parity split of the proof of Theorem 4.4 work.

Formalization Note As for Lemma 4.6, the Lean statement holds for every ranking $\tau$ in place of $\succ'_i$ and involves no valuations. With 0-based $r$ (the paper's $r-1$) it reads (roundRobin σ j ∩ (allocBefore σ' (r*n + i) \ allocBefore σ' i)).card ≤ 2 * r for r < k, where $S'_0$ is allocBefore σ' i.

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 τ.