Keyword: fair-division

Theorem Acyclic Envy Graph Has a Source staged

Definition Additive Valuation formalized

Definition Allocation formalized

Lemma Basic Welfare Lemmas staged

Definition Best-Good Selection formalized

Definition Bundle Rotation formalized

Lemma CDF of a Non-Atomic Finite Measure on ℝ Is Continuous staged

Definition Cake Valuation formalized

Definition Cardinal Fair-Division Instance formalized

Definition Cardinal-Instance Fairness and Welfare Wrappers formalized

Theorem Chooser Is Always Envy-Free staged

Definition Cut-and-Choose Allocation and Fair Cut Point formalized

Theorem Cut-and-Choose Is Envy-Free at a Fair Cut staged

Theorem Cut-and-Choose Output Is a Complete Partition staged

Theorem Cutter Does Not Envy at a Fair Cut staged

Theorem Decidable Fairness Checkers staged

Definition Divisible Allocation formalized

Definition Divisible Cardinal Instance formalized

Definition Divisible Envy-Free, Proportional, Equitable Predicates formalized

Definition Divisible Measure Instance formalized

Definition Divisible Ordinal Instance formalized

Lemma Dubins–Spanier Inductive Step staged

Theorem Dubins–Spanier Proportional Existence staged

Theorem Dubins–Spanier as a Rule on Measure Instances staged

Theorem EF + Proportional Existence (Stromquist Corollary) staged

Theorem EF Impossibility — Two Agents, One Good staged

Theorem EF ⇒ EFX (Monotone Valuations) staged

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

Theorem EF ⇒ Proportional (Measure Valuations) 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 Egalitarian (Maximin) Welfare formalized

Lemma Egalitarian Welfare Lower-Bounds Utilitarian Welfare 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 Envy-Free Allocation formalized

Theorem Envy-Free Existence (Stromquist, n Agents) staged

Definition Equitable Allocation formalized

Lemma Fair Assignment from a Common KKM Point staged

Theorem Fair Cut Point Exists staged

Definition Fair Division Instance formalized

Definition Fair Division Solution Concept and Rule formalized

Lemma IVT — Cut Point Exists for Non-Atomic Measures on [0,1] 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

Definition Measure Valuation formalized

Theorem Measure-Instance EF ↔ Real-Valued Cardinal EF staged

Theorem Measure-Instance Existence Wrappers staged

Lemma Non-Atomicity Is Preserved by Subtype.val Pushforward staged

Lemma Normalized Measure Valuation ↔ Probability Measure staged

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

Theorem PROP ⇒ α-MMS (Additive Valuations) staged

Definition Pareto Optimal Allocation formalized

Definition Pareto-Domination Count Termination Measure formalized

Lemma Piece-Value Function Is Continuous on the Division Simplex staged

Definition Proportional Allocation formalized

Theorem Proportional Existence on [0,1] (n Agents) staged

Definition Round-Robin Allocation formalized

Theorem Round-Robin Is EF1 staged

Theorem Round-Robin Output Is a Complete Partition staged

Definition Share Instance (No-Externality Model) formalized

Definition Stromquist Agent-Preference Union U(i) formalized

Definition Stromquist Pieces from the Division Simplex formalized

Definition Stromquist Preference Sets A(i, j) formalized

Definition Stromquist Shifted-Cell Approximation staged

Definition Stromquist Unique-Preference Sets B(i, j) formalized

Theorem Stromquist — Unusual Case (Shifted-Cell Limit) staged

Theorem Stromquist — Usual Case (U Covers the Simplex) staged

Theorem Two-Agent EF Existence via Cut-and-Choose staged

Definition Utilitarian Welfare and Utilitarian Optimality formalized

Definition Utility Represents Share Preference formalized

Definition α-MMS Allocation formalized

Theorem α-MMS — Monotonicity and Endpoint Lemmas staged