Social Choice.Fair Division.Divisible.Stromquist

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

Lemma Fair Assignment from a Common KKM Point staged

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

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