Keyword: envy-free

Theorem Chooser Is Always Envy-Free staged

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

Theorem Cutter Does Not Envy at a Fair Cut staged

Definition Divisible Envy-Free, Proportional, Equitable Predicates formalized

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 Envy-Free Allocation formalized

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

Lemma Fair Assignment from a Common KKM Point staged

Definition Indivisible Envy-Free formalized

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

Theorem Measure-Instance Existence Wrappers staged

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