EconCSLib.SocialChoice.FairDivision.Basic

Generic fair-division vocabulary as a structured special case of social choice.

This file introduces:

• Allocation N S as the common shape of an allocation
• Instance for fully general fair-division problems with preferences over complete allocations
• ShareInstance for the standard no-externality model where each agent ranks only the share they receive
• the lift ShareInstance.toInstance, showing how fair division fits into the generic social-choice layer

@[reducible, inline]

abbrev SocialChoice.FairDivision.Allocation (N : Type u_1) (S : Type u_2) : Type (max u_1 u_2)

A fair-division allocation assigns each agent a share.

Equations

• SocialChoice.FairDivision.Allocation N S = (N → S)

structure SocialChoice.FairDivision.Instance (N : Type u_1) (R : Type u_2) (S : Type u_3) : Type (max (max u_1 u_2) u_3)

A fully general fair-division instance.

This allows preferences over complete allocations, so it can express externalities or other global allocation comparisons.

• resource : R

  Resource-side data for the instance.

• feasible : Allocation N S → Prop

  Feasible allocations for the given resource data.

• pref : N → Pref (Allocation N S)

  Each agent's preference over complete allocations.

structure SocialChoice.FairDivision.ShareInstance (N : Type u_1) (R : Type u_2) (S : Type u_3) : Type (max (max u_1 u_2) u_3)

A no-externality fair-division instance where each agent ranks only the share they personally receive.

• resource : R

  Resource-side data for the instance.

• feasible : Allocation N S → Prop

  Feasible allocations for the given resource data.

• sharePref : N → Pref S

  Each agent's preference over individual shares.

def SocialChoice.FairDivision.ShareInstance.toInstance {N : Type u_1} {R : Type u_2} {S : Type u_3} (I : ShareInstance N R S) : Instance N R S

Lift a no-externality fair-division instance to a fully general allocation-preference instance by comparing allocations pointwise through the share assigned to the evaluating agent.

Equations

• One or more equations did not get rendered due to their size.

def SocialChoice.FairDivision.SolutionConcept (N : Type u_1) (R : Type u_2) (S : Type u_3) : Type (max (max (max (max u_3 u_2) u_1) u_3) u_1)

A fair-division solution concept is a predicate selecting acceptable allocations relative to a fully general instance.

Equations

• SocialChoice.FairDivision.SolutionConcept N R S = (SocialChoice.FairDivision.Instance N R S → SocialChoice.FairDivision.Allocation N S → Prop)

def SocialChoice.FairDivision.Rule (N : Type u_1) (R : Type u_2) (S : Type u_3) : Type (max (max (max u_3 u_2) u_1) u_1 u_3)

A fair-division rule returns a feasible allocation for every instance.

Equations

• SocialChoice.FairDivision.Rule N R S = ((I : SocialChoice.FairDivision.Instance N R S) → { A : SocialChoice.FairDivision.Allocation N S // I.feasible A })