Social Choice.Fair Division.Indivisible.Algorithms

Theorem Acyclic Envy Graph Has a Source staged

Definition Best-Good Selection formalized

Definition Bundle Rotation formalized

Definition Eliminate All Envy Cycles formalized

Definition Envy Cycle formalized

Definition Envy Relation and Sources formalized

Definition Envy-Cycle Elimination Algorithm formalized

Theorem Envy-Cycle Elimination Produces EF1 staged

Definition Pareto-Domination Count Termination Measure formalized

Definition Round-Robin Allocation formalized

Theorem Round-Robin Is EF1 staged

Theorem Round-Robin Output Is a Complete Partition staged