EconCSLib.SocialChoice.FairDivision.Indivisible.RoundRobin

The choice round-robin algorithm and its EF1 correctness proof, stated on the canonical bundled AdditiveInstance interface.

Main definitions

• bestGood — argmax helper: an element of s maximizing an agent's item weight
• roundRobinAux — recursive core: agents take turns picking their best remaining good
• roundRobinAllocation — the complete round-robin allocation for an additive instance
• roundRobinRule — a feasible-allocation rule induced by round-robin

Main results

• roundRobinAllocation_isAllocation — the output is a valid partition of I.allGoods
• roundRobinAllocation_isEF1 — the output satisfies EF1 for nonnegative weights
• roundRobinRule_isEF1 — rule-style EF1 correctness

Algorithm

Agents are ordered 0, 1, ..., n-1, 0, 1, ... (cycling mod n). In each step the current agent picks their highest-weight remaining good. The implementation recurses on remaining.card with accumulator A : Allocation (Fin n) G.

EF1 proof outline

Fix distinct agents i, j : Fin n.

Case i.val < j.val (i picks before j in every round): When i picks their r-th good i_r in round r, agent j's round-r good j_r is still in the pool (j hasn't picked yet that round). Since i picks optimally, v_i(i_r) ≥ v_i(j_r). Summing over rounds: v_i(A_i) ≥ v_i(A_j) — agent i does not envy j at all (stronger than EF1). Any good in A_j is therefore a valid EF1 witness (use monotonicity: removing a good can only decrease value).

Case j.val < i.val (j picks before i in every round): When i picks their r-th good i_r in round r, agent j's next good j_{r+1} is still in the pool (j picks in round r+1, after i picks in round r). So v_i(i_r) ≥ v_i(j_{r+1}). Telescoping over r = 0, …, |A_j| − 2: v_i(A_i) ≥ Σ_r v_i(j_{r+1}) = v_i(A_j) − v_i(j_0), i.e., v_i(A_j \ {j_0}) ≤ v_i(A_i), where j_0 is j's first picked good (EF1 witness).

Proof technique

All proofs use strong induction on remaining.card via Finset.strongInductionOn, with case splits on turn = i, turn = j, turn ≠ i ∧ turn ≠ j handled via Function.update_apply.

The EF1 correctness proofs use two-part invariants maintained across rounds:

• roundRobin_noEnvy_of_earlier maintains v_i(A j) ≤ v_i(A i) (no-envy) plus a headroom condition v_i(A j) + w_i(g) ≤ v_i(A i) for all remaining g, active when agent i has picked in the current cycle but j has not yet (i.val < turn.val ≤ j.val).

• roundRobin_ef1_of_later maintains a two-phase invariant: Phase 1 (before j's first pick) and Phase 2 (after j picks witness g0: v_i(A j \ {g0}) ≤ v_i(A i) with conditional headroom guarded by i.val < turn.val ∨ turn.val ≤ j.val).

References

• Lipton et al., "On Approximately Fair Allocations of Indivisible Goods" (EC 2004)
• Nisan et al., Algorithmic Game Theory, Chapter 11

Raw implementation layer

The public algorithm below is stated on AdditiveInstance. The recursive proof machinery is parameterized by the raw induced valuation to keep the induction lemmas independent of bundled-record projection noise.

Best-item selection

Round-robin algorithm

Unfolding lemmas

Partition properties

EF1 correctness

Bundled additive-instance API

noncomputable def SocialChoice.FairDivision.Indivisible.bestGood {n : ℕ} {G : Type u_1} [DecidableEq G] (I : AdditiveInstance (Fin n) G) (i : Fin n) (s : Finset G) (hs : s.Nonempty) : G

bestGood I i s hs is a good in s maximizing agent i's item weight.

Equations

• SocialChoice.FairDivision.Indivisible.bestGood I i s hs = SocialChoice.FairDivision.Indivisible.rawBestGood✝ I.toAdditiveValuation i s hs

theorem SocialChoice.FairDivision.Indivisible.bestGood_mem {n : ℕ} {G : Type u_1} [DecidableEq G] (I : AdditiveInstance (Fin n) G) (i : Fin n) (s : Finset G) (hs : s.Nonempty) : bestGood I i s hs ∈ s

bestGood lies in the candidate set.

theorem SocialChoice.FairDivision.Indivisible.bestGood_le {n : ℕ} {G : Type u_1} [DecidableEq G] (I : AdditiveInstance (Fin n) G) (i : Fin n) (s : Finset G) (hs : s.Nonempty) {g : G} (hg : g ∈ s) : I.weight i g ≤ I.weight i (bestGood I i s hs)

Every candidate good has no larger weight than bestGood.

noncomputable def SocialChoice.FairDivision.Indivisible.roundRobinAux {n : ℕ} {G : Type u_1} [NeZero n] [DecidableEq G] (I : AdditiveInstance (Fin n) G) (turn : Fin n) (remaining : Finset G) (A : Allocation (Fin n) G) : Allocation (Fin n) G

Recursive core of round-robin for bundled additive instances.

Equations

• SocialChoice.FairDivision.Indivisible.roundRobinAux I turn remaining A = SocialChoice.FairDivision.Indivisible.rawRoundRobinAux✝ I.toAdditiveValuation turn remaining A

noncomputable def SocialChoice.FairDivision.Indivisible.roundRobinAllocation {n : ℕ} {G : Type u_1} [NeZero n] [DecidableEq G] (I : AdditiveInstance (Fin n) G) : Allocation (Fin n) G

The complete choice round-robin allocation for a bundled additive instance.

Equations

• SocialChoice.FairDivision.Indivisible.roundRobinAllocation I = SocialChoice.FairDivision.Indivisible.roundRobinAux I ⟨0, ⋯⟩ I.allGoods fun (x : Fin n) => ∅

noncomputable def SocialChoice.FairDivision.Indivisible.roundRobinRule {n : ℕ} {G : Type u_1} [NeZero n] [DecidableEq G] (I : AdditiveInstance (Fin n) G) : { A : Allocation (Fin n) G // I.feasible A }

Round-robin as a feasible-allocation rule on bundled additive instances.

Equations

• SocialChoice.FairDivision.Indivisible.roundRobinRule I = ⟨SocialChoice.FairDivision.Indivisible.roundRobinAllocation I, ⋯⟩

theorem SocialChoice.FairDivision.Indivisible.roundRobinAllocation_isAllocation {n : ℕ} {G : Type u_1} [NeZero n] [DecidableEq G] (I : AdditiveInstance (Fin n) G) : IsAllocation I.allGoods (roundRobinAllocation I)

roundRobinAllocation produces a complete partition of the instance goods.

theorem SocialChoice.FairDivision.Indivisible.roundRobinAllocation_isEF1 {n : ℕ} {G : Type u_1} [NeZero n] [DecidableEq G] (I : AdditiveInstance (Fin n) G) (hnn : ∀ (i : Fin n) (g : G), 0 ≤ I.weight i g) : I.IsEF1 (roundRobinAllocation I)

Round-robin gives EF1 for additive instances with nonnegative item weights.

theorem SocialChoice.FairDivision.Indivisible.roundRobinRule_isEF1 {n : ℕ} {G : Type u_1} [NeZero n] [DecidableEq G] (I : AdditiveInstance (Fin n) G) (hnn : ∀ (i : Fin n) (g : G), 0 ≤ I.weight i g) : I.IsEF1 ↑(roundRobinRule I)

The bundled round-robin rule is EF1 under nonnegative item weights.