Keyword: indivisible

Theorem Acyclic Envy Graph Has a Source staged

Definition Additive Valuation formalized

Definition Best-Good Selection formalized

Definition Bundle Rotation formalized

Theorem Decidable Fairness Checkers staged

Theorem EF Impossibility — Two Agents, One Good staged

Theorem EF ⇒ EFX (Monotone Valuations) staged

Theorem EF ⇒ PROP (Additive Valuations, Complete Allocations) staged

Definition EF1 — Envy-Free Up to One Good formalized

Theorem EFX Existence — 2 Agents, 2 Goods staged

Theorem EFX Existence — Two Agents, Any Finite Good Set staged

Theorem EFX from No-Envy + Monotonicity staged

Lemma EFX from a Singleton-Bundle Sufficient Condition staged

Definition EFX — Envy-Free Up to Any Good formalized

Theorem EFX ⇒ EF1 staged

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 Indivisible Additive Instance formalized

Definition Indivisible Allocation formalized

Definition Indivisible Cardinal Instance formalized

Definition Indivisible Egalitarian (Maximin) Welfare formalized

Definition Indivisible Envy-Free formalized

Definition Indivisible Equitable formalized

Definition Indivisible Ordinal Instance formalized

Definition Indivisible Pareto Optimal formalized

Definition Indivisible Proportional formalized

Definition Indivisible Utilitarian Welfare formalized

Definition Indivisible Valuation formalized

Theorem IsMaxminShare ↔ IsAlphaMMS 1 staged

Lemma MMS Value — Basic Bounds staged

Definition Maximin Share (MMS) Allocation formalized

Definition Maximin Share Value formalized

Theorem PROP ⇒ MMS (Additive Valuations, Complete Allocations) staged

Theorem PROP ⇒ α-MMS (Additive Valuations) 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

Definition α-MMS Allocation formalized

Theorem α-MMS — Monotonicity and Endpoint Lemmas staged