EconCSLib.SocialChoice.FairDivision.Indivisible.EnvyCycle

The envy-cycle elimination algorithm and its EF1 correctness proof, stated on the canonical bundled AdditiveInstance interface.

Main definitions

• envies v A i j — agent i strictly envies agent j: v_i(A_i) < v_i(A_j)
• isSource v A i — i has in-degree 0 in the envy graph (no one envies i)
• isEnvyCycle v A l — l is a directed cycle in the envy graph
• hasEnvyCycle v A — the envy graph contains at least one directed cycle
• rotateBundles A l — rotate bundles around cycle l
• eliminateAllCycles v A — iterate rotation until no envy cycle remains
• findSource v A h — a source in the acyclic envy graph
• envyCycleAllocation I — full bundled algorithm: process I.allGoods in list order
• envyCycleRule I — the algorithm as a feasible-allocation rule

Main results

• rotateBundles_not_mem — agents outside the cycle are unaffected by rotation
• rotateBundles_isAllocation — rotation preserves the partition property
• rotateBundles_improves — every agent in the cycle strictly improves after rotation
• rotateBundles_nondecreasing — no agent loses value under a rotation step
• eliminateAllCycles_acyclic — after elimination, the envy graph contains no cycle
• eliminateAllCycles_isAllocation — valid allocations are preserved by elimination
• eliminateAllCycles_nondecreasing — agent values do not decrease under elimination
• eliminateAllCycles_eq_of_acyclic — elimination is the identity on already-acyclic allocations
• acyclic_has_source — a finite acyclic directed graph always has a source
• findSource_isSource — the agent returned by findSource satisfies isSource
• envyCycleAllocation_isAllocation — output is a valid complete allocation
• envyCycleAllocation_isEF1 — output satisfies EF1 for nonnegative additive weights
• envyCycleRule_isEF1 — rule-style EF1 correctness

Algorithm outline

Process a list of goods one at a time. The current partial allocation A is kept cycle-free throughout (loop invariant). Each step is:

1. Let A_dag = eliminateAllCycles v A (no-op if A is already acyclic).
2. Find a source s in the envy graph of A_dag (exists because A_dag is a DAG; see acyclic_has_source).
3. Give the next good g to s: update A_dag s ↦ insert g (A_dag s).
4. Eliminate any new envy cycles: eliminateAllCycles v (Function.update A_dag s ...).

Raw implementation layer

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

EF1 invariant

After each complete step (add good + eliminate cycles), the partial allocation is envy-free (EF) among all agents with nonempty bundles. This is maintained because:

• Before adding g, no agent envied the source s (source property of step 2).
• Adding g to s may introduce new envy towards s; these are resolved in step 4.
• Envy between non-source agents is unchanged by steps 2–4.

When the last good is allocated the allocation is EF among nonempty-bundle agents, which implies EF1 globally (the guard (A j).Nonempty in IsEF1 covers agents with A j = ∅).

Termination of eliminateAllCycles

Termination is witnessed by the Pareto domination count: the number of allocations B such that every agent weakly prefers B to the current allocation A. Each rotation step strictly improves at least one agent (and weakly improves all), so this count strictly decreases. Since [Fintype N] and [Fintype G] make the set of allocations finite, the count is bounded and the loop terminates.

References

• Lipton et al., "On Approximately Fair Allocations of Indivisible Goods" (EC 2004) [L+04]
• Nisan et al., Algorithmic Game Theory, Chapter 12
• Bouveret, Chevaleyre, Maudet — COMSOC Handbook, Ch. 12 [BCM]

Envy relation

def SocialChoice.FairDivision.Indivisible.envies {N : Type u_1} {G : Type u_2} (v : Valuation N G) (A : Allocation N G) (i j : N) : Prop

Agent i envies agent j under valuation v and allocation A: they strictly prefer j's bundle over their own.

envies v A i j ↔ v_i(A_i) < v_i(A_j).

An allocation is envy-free (IsEnvyFree) iff no agent envies any other. [L+04]

Equations

• SocialChoice.FairDivision.Indivisible.envies v A i j = (v.val i (A i) < v.val i (A j))

theorem SocialChoice.FairDivision.Indivisible.envies_irrefl {N : Type u_1} {G : Type u_2} (v : Valuation N G) (A : Allocation N G) (i : N) : ¬envies v A i i

An agent cannot envy themselves: envies v A i i is always false.

theorem SocialChoice.FairDivision.Indivisible.envies_ne {N : Type u_1} {G : Type u_2} (v : Valuation N G) (A : Allocation N G) {i j : N} (h : envies v A i j) : i ≠ j

Envy implies distinct agents: if i envies j then i ≠ j.

Sources in the envy graph

def SocialChoice.FairDivision.Indivisible.isSource {N : Type u_1} {G : Type u_2} (v : Valuation N G) (A : Allocation N G) (i : N) : Prop

Agent i is a source in the envy graph: no other agent envies i.

Equivalently, i has in-degree 0 in the envy graph. Sources always exist in finite acyclic graphs (see acyclic_has_source). Giving a new good to a source is the key step in the algorithm: since no agent envied the source before, the source can only attract new envy from the added good — not from pre-existing bundles.

Equations

• SocialChoice.FairDivision.Indivisible.isSource v A i = ∀ (j : N), ¬SocialChoice.FairDivision.Indivisible.envies v A j i

theorem SocialChoice.FairDivision.Indivisible.IsEnvyFree.isSource_all {N : Type u_1} {G : Type u_2} (v : Valuation N G) (A : Allocation N G) (hef : IsEnvyFree v A) (i : N) : isSource v A i

In an envy-free allocation, every agent is a source.

Envy cycles

def SocialChoice.FairDivision.Indivisible.isEnvyCycle {N : Type u_1} {G : Type u_2} (v : Valuation N G) (A : Allocation N G) (l : List N) : Prop

A list l : List N is a directed envy cycle under v and A if:

• l is nonempty (0 < l.length),
• all elements are distinct (l.Nodup), and
• every consecutive pair (with wrap-around from last to first) is an envy edge.

For l = [i₀, i₁, ..., iₖ₋₁]: agent iⱼ envies i_{(j+1) mod k} for all j. In particular iₖ₋₁ envies i₀, closing the directed cycle. [L+04]

Equations

• One or more equations did not get rendered due to their size.

def SocialChoice.FairDivision.Indivisible.hasEnvyCycle {N : Type u_1} {G : Type u_2} (v : Valuation N G) (A : Allocation N G) : Prop

The envy graph has a cycle: some nonempty list forms a directed envy cycle.

Equations

• SocialChoice.FairDivision.Indivisible.hasEnvyCycle v A = ∃ (l : List N), SocialChoice.FairDivision.Indivisible.isEnvyCycle v A l

theorem SocialChoice.FairDivision.Indivisible.isEnvyCycle_length_ge_two {N : Type u_1} {G : Type u_2} (v : Valuation N G) (A : Allocation N G) (l : List N) (hcyc : isEnvyCycle v A l) : 2 ≤ l.length

A directed envy cycle must have length at least 2. A singleton [i] would require i to envy itself, contradicting irreflexivity of <.

theorem SocialChoice.FairDivision.Indivisible.isSource_not_mem_envyCycle {N : Type u_1} {G : Type u_2} (v : Valuation N G) (A : Allocation N G) (i : N) (hs : isSource v A i) (l : List N) (hcyc : isEnvyCycle v A l) : i ∉ l

If i is a source, it cannot participate in any envy cycle.

Bundle rotation

noncomputable def SocialChoice.FairDivision.Indivisible.rotateBundles {N : Type u_1} {G : Type u_2} [DecidableEq N] (A : Allocation N G) (l : List N) : Allocation N G

Rotate bundles around a cycle l = [i₀, i₁, ..., iₖ₋₁]: agent iⱼ receives the bundle currently held by i_{(j+1) mod k}. Agents not in l are unaffected.

Requires [DecidableEq N] for Function.update. Correctness lemmas assume l.Nodup (so each agent appears at most once and the rotation is well-defined).

After rotation along an envy cycle, every participating agent receives a bundle they strictly preferred: iⱼ gets A i_{j+1} and envies v A iⱼ i_{j+1} guarantees v_{iⱼ}(A iⱼ) < v_{iⱼ}(A i_{j+1}). [L+04]

Equations

• One or more equations did not get rendered due to their size.

Lemmas about rotateBundles

theorem SocialChoice.FairDivision.Indivisible.rotateBundles_not_mem {N : Type u_1} {G : Type u_2} [DecidableEq N] (A : Allocation N G) (l : List N) (i : N) (h : i ∉ l) : rotateBundles A l i = A i

Agents not in the cycle are unaffected by bundle rotation.

theorem SocialChoice.FairDivision.Indivisible.rotateBundles_mem {N : Type u_1} {G : Type u_2} [DecidableEq N] (A : Allocation N G) (l : List N) (i : N) (h : i ∈ l) : ∃ (k : Fin l.length), l.get k = i ∧ ∃ (k' : Fin l.length), ↑k' = (↑k + 1) % l.length ∧ rotateBundles A l i = A (l.get k')

Each agent in the cycle receives their successor's bundle. Concretely, if i = l.get k, then rotateBundles A l i = A (l.get k') where k' = (k.val + 1) % l.length.

theorem SocialChoice.FairDivision.Indivisible.rotateBundles_isAllocation {N : Type u_1} {G : Type u_2} [DecidableEq N] [DecidableEq G] [Fintype N] {allGoods : Finset G} {A : Allocation N G} (hA : IsAllocation allGoods A) (l : List N) (hnd : l.Nodup) : IsAllocation allGoods (rotateBundles A l)

Bundle rotation preserves the partition property.

Proof sketch: the goods held by cycle participants are permuted cyclically. The disjointness and completeness properties of the partition are maintained because the multiset of bundles is merely rearranged — the same goods appear in the same total quantity, just redistributed among cycle agents.

theorem SocialChoice.FairDivision.Indivisible.rotateBundles_improves {N : Type u_1} {G : Type u_2} [DecidableEq N] (v : Valuation N G) (A : Allocation N G) (l : List N) (hcyc : isEnvyCycle v A l) (i : N) (hi : i ∈ l) : v.val i (A i) < v.val i (rotateBundles A l i)

After rotating along an envy cycle l, every agent in l strictly improves.

Proof: agent iⱼ in the cycle satisfies envies v A iⱼ i_{j+1}, i.e., v_{iⱼ}(A iⱼ) < v_{iⱼ}(A i_{j+1}). After rotation, iⱼ holds A i_{j+1}, so their new value strictly exceeds their old value.

theorem SocialChoice.FairDivision.Indivisible.rotateBundles_nondecreasing {N : Type u_1} {G : Type u_2} [DecidableEq N] (v : Valuation N G) (A : Allocation N G) (l : List N) (hcyc : isEnvyCycle v A l) (i : N) : v.val i (A i) ≤ v.val i (rotateBundles A l i)

Bundle rotation does not decrease any agent's value. Cycle participants strictly improve (see rotateBundles_improves); non-participants are unchanged.

Pareto domination count (termination measure)

noncomputable def SocialChoice.FairDivision.Indivisible.paretoDomCount {N : Type u_1} {G : Type u_2} [Fintype N] [Fintype G] (v : Valuation N G) (A : Allocation N G) : ℕ

The number of allocations that weakly Pareto-dominate A: every agent weakly prefers B's assignment over A's. This count strictly decreases with each envy-cycle rotation, providing the termination measure for eliminateAllCycles.

Equations

• SocialChoice.FairDivision.Indivisible.paretoDomCount v A = {B : N → Finset G | ∀ (i : N), v.val i (A i) ≤ v.val i (B i)}.card

theorem SocialChoice.FairDivision.Indivisible.paretoDomSet_subset {N : Type u_1} {G : Type u_2} [Fintype N] [Fintype G] (v : Valuation N G) (A A' : Allocation N G) (h : ∀ (i : N), v.val i (A i) ≤ v.val i (A' i)) : {B : N → Finset G | ∀ (i : N), v.val i (A' i) ≤ v.val i (B i)} ⊆ {B : N → Finset G | ∀ (i : N), v.val i (A i) ≤ v.val i (B i)}

The Pareto domination set of A' is a subset of that of A when A' weakly Pareto-dominates A.

theorem SocialChoice.FairDivision.Indivisible.self_mem_paretoDomSet {N : Type u_1} {G : Type u_2} [Fintype N] [Fintype G] (v : Valuation N G) (A : Allocation N G) : A ∈ {B : N → Finset G | ∀ (i : N), v.val i (A i) ≤ v.val i (B i)}

A belongs to its own Pareto domination set (by reflexivity).

theorem SocialChoice.FairDivision.Indivisible.not_mem_paretoDomSet_of_strict {N : Type u_1} {G : Type u_2} [Fintype N] [Fintype G] (v : Valuation N G) (A A' : Allocation N G) (_hweak : ∀ (i : N), v.val i (A i) ≤ v.val i (A' i)) (hstrict : ∃ (j : N), v.val j (A j) < v.val j (A' j)) : A ∉ {B : N → Finset G | ∀ (i : N), v.val i (A' i) ≤ v.val i (B i)}

If A' strictly Pareto-improves over A (weakly for all, strictly for some agent), then A is NOT in the Pareto domination set of A'.

theorem SocialChoice.FairDivision.Indivisible.rotateBundles_paretoDomCount_lt {N : Type u_1} {G : Type u_2} [Fintype N] [Fintype G] [DecidableEq N] (v : Valuation N G) (A : Allocation N G) (l : List N) (hcyc : isEnvyCycle v A l) : paretoDomCount v (rotateBundles A l) < paretoDomCount v A

Rotation along an envy cycle strictly decreases the Pareto domination count.

Cycle elimination

noncomputable def SocialChoice.FairDivision.Indivisible.eliminateAllCycles {N : Type u_1} {G : Type u_2} [Fintype N] [Fintype G] [DecidableEq N] (v : Valuation N G) (A : Allocation N G) : Allocation N G

Repeatedly rotate envy cycles until none remain, producing a cycle-free allocation.

eliminateAllCycles v A is an allocation reachable from A by a finite sequence of bundle rotations that contains no directed envy cycle.

Termination is witnessed by the paretoDomCount measure: each rotation step strictly decreases the number of allocations that weakly Pareto-dominate the current allocation. Since this count is a natural number, the process terminates.

Key properties (proved below):

• eliminateAllCycles_acyclic: the output is cycle-free.
• eliminateAllCycles_isAllocation: the partition property is preserved.
• eliminateAllCycles_nondecreasing: no agent's value decreases.
• eliminateAllCycles_eq_of_acyclic: the identity on already-acyclic inputs.

Equations

• One or more equations did not get rendered due to their size.

theorem SocialChoice.FairDivision.Indivisible.eliminateAllCycles_unfold {N : Type u_1} {G : Type u_2} [Fintype N] [Fintype G] [DecidableEq N] (v : Valuation N G) (A : Allocation N G) : eliminateAllCycles v A = if h : hasEnvyCycle v A then eliminateAllCycles v (rotateBundles A (Classical.choose h)) else A

Unfolding lemma for eliminateAllCycles: if a cycle exists, rotate and recurse; otherwise return the current allocation.

Lemmas about eliminateAllCycles

theorem SocialChoice.FairDivision.Indivisible.eliminateAllCycles_acyclic {N : Type u_1} {G : Type u_2} [Fintype N] [Fintype G] [DecidableEq N] (v : Valuation N G) (A : Allocation N G) : ¬hasEnvyCycle v (eliminateAllCycles v A)

After cycle elimination, the envy graph is acyclic. This is the defining correctness property of eliminateAllCycles. [L+04]

theorem SocialChoice.FairDivision.Indivisible.eliminateAllCycles_isAllocation {N : Type u_1} {G : Type u_2} [Fintype N] [Fintype G] [DecidableEq N] [DecidableEq G] (v : Valuation N G) {allGoods : Finset G} {A : Allocation N G} (hA : IsAllocation allGoods A) : IsAllocation allGoods (eliminateAllCycles v A)

Cycle elimination preserves the partition property. Each rotation step preserves IsAllocation by rotateBundles_isAllocation, and the composition of finitely many such steps preserves it inductively.

theorem SocialChoice.FairDivision.Indivisible.eliminateAllCycles_nondecreasing {N : Type u_1} {G : Type u_2} [Fintype N] [Fintype G] [DecidableEq N] [DecidableEq G] (v : Valuation N G) (A : Allocation N G) (i : N) : v.val i (A i) ≤ v.val i (eliminateAllCycles v A i)

Cycle elimination does not decrease any agent's value (for additive nonneg valuations).

Each rotation step strictly improves participating agents and leaves others unchanged, so the entire sequence of rotations is value-nondecreasing for every agent.

theorem SocialChoice.FairDivision.Indivisible.eliminateAllCycles_eq_of_acyclic {N : Type u_1} {G : Type u_2} [Fintype N] [Fintype G] [DecidableEq N] (v : Valuation N G) (A : Allocation N G) (h : ¬hasEnvyCycle v A) : eliminateAllCycles v A = A

Cycle elimination is a fixed point on acyclic inputs: if A already has no envy cycle, then eliminateAllCycles v A = A (no rotation is performed).

Sources

theorem SocialChoice.FairDivision.Indivisible.acyclic_has_source {N : Type u_1} {G : Type u_2} [Fintype N] [Nonempty N] (v : Valuation N G) (A : Allocation N G) (hdag : ¬hasEnvyCycle v A) : ∃ (i : N), isSource v A i

A finite directed graph with no directed cycle has at least one source (a node with in-degree 0).

Proof sketch: start from any agent i₀. If i₀ is a source, done. Otherwise pick any i₁ that envies i₀. Repeat: if i₁ is a source, done; else pick i₂ envying i₁. Since N is finite, this walk must revisit some node, yielding a directed cycle — contradicting hdag. Hence the walk must terminate at a source.

[BCM Ch.12; standard directed graph theory]

noncomputable def SocialChoice.FairDivision.Indivisible.findSource {N : Type u_1} {G : Type u_2} [Fintype N] [Nonempty N] (v : Valuation N G) (A : Allocation N G) (hdag : ¬hasEnvyCycle v A) : N

Given a proof that the envy graph of A is acyclic, returns a source agent. The specific agent chosen is unspecified beyond satisfying isSource.

Equations

• SocialChoice.FairDivision.Indivisible.findSource v A hdag = Classical.choose ⋯

theorem SocialChoice.FairDivision.Indivisible.findSource_isSource {N : Type u_1} {G : Type u_2} [Fintype N] [Nonempty N] (v : Valuation N G) (A : Allocation N G) (hdag : ¬hasEnvyCycle v A) : isSource v A (findSource v A hdag)

The agent returned by findSource is indeed a source in the envy graph of A.

Envy-cycle elimination algorithm

Correctness theorems

Helper lemmas for EF1

Bundled additive-instance API

noncomputable def SocialChoice.FairDivision.Indivisible.envyCycleAllocation {N : Type u_1} {G : Type u_2} [Fintype N] [Fintype G] [Nonempty N] [DecidableEq N] [DecidableEq G] (I : AdditiveInstance N G) : Allocation N G

The complete envy-cycle-elimination allocation for a bundled additive instance.

Equations

• SocialChoice.FairDivision.Indivisible.envyCycleAllocation I = SocialChoice.FairDivision.Indivisible.rawEnvyCycleElimination✝ I.toAdditiveValuation.toValuation I.allGoods.toList

noncomputable def SocialChoice.FairDivision.Indivisible.envyCycleRule {N : Type u_1} {G : Type u_2} [Fintype N] [Fintype G] [Nonempty N] [DecidableEq N] [DecidableEq G] (I : AdditiveInstance N G) : { A : Allocation N G // I.feasible A }

Envy-cycle elimination as a feasible-allocation rule on bundled additive instances.

Equations

• SocialChoice.FairDivision.Indivisible.envyCycleRule I = ⟨SocialChoice.FairDivision.Indivisible.envyCycleAllocation I, ⋯⟩

theorem SocialChoice.FairDivision.Indivisible.envyCycleAllocation_isAllocation {N : Type u_1} {G : Type u_2} [Fintype N] [Fintype G] [Nonempty N] [DecidableEq N] [DecidableEq G] (I : AdditiveInstance N G) : IsAllocation I.allGoods (envyCycleAllocation I)

envyCycleAllocation produces a complete partition of the instance goods.

theorem SocialChoice.FairDivision.Indivisible.envyCycleAllocation_isEF1 {N : Type u_1} {G : Type u_2} [Fintype N] [Fintype G] [Nonempty N] [DecidableEq N] [DecidableEq G] (I : AdditiveInstance N G) (hnn : ∀ (i : N) (g : G), 0 ≤ I.weight i g) : I.IsEF1 (envyCycleAllocation I)

Envy-cycle elimination gives EF1 for additive instances with nonnegative item weights.

theorem SocialChoice.FairDivision.Indivisible.envyCycleRule_isEF1 {N : Type u_1} {G : Type u_2} [Fintype N] [Fintype G] [Nonempty N] [DecidableEq N] [DecidableEq G] (I : AdditiveInstance N G) (hnn : ∀ (i : N) (g : G), 0 ≤ I.weight i g) : I.IsEF1 ↑(envyCycleRule I)

The bundled envy-cycle-elimination rule is EF1 under nonnegative item weights.