EconCSLib.SocialChoice.FairDivision.Indivisible.Checker

Noncomputable Bool-valued reflection helpers for indivisible-goods fairness predicates.

For finite instances (finite agents and finite goods), these definitions package each fairness predicate as a Boolean together with a correctness theorem (iff). They are noncomputable because valuations are real-valued; they are not intended for #eval or native_decide.

Main definitions

• isEnvyFree — Boolean reflection helper for IsEnvyFree
• isEF1 — Boolean reflection helper for IsEF1
• isEFX — Boolean reflection helper for IsEFX
• isProportional — Boolean reflection helper for IsProportional

Main results

• isEnvyFree_iff, isEF1_iff, isEFX_iff, isProportional_iff — soundness and completeness of each checker.

Typeclass requirements

• [Fintype N] and [DecidableEq N] — iterate over agents
• [DecidableEq G] — Finset operations on bundles (sdiff, membership) The value codomain is fixed to ℝ, so no valuation-ordering typeclasses are needed.

References

• Nisan et al., Algorithmic Game Theory, Chapter 11

Envy-freeness reflection

noncomputable def SocialChoice.FairDivision.Indivisible.isEnvyFree {N : Type u_1} {G : Type u_2} [Fintype N] (v : Valuation N G) (A : Allocation N G) : Bool

Noncomputable envy-free Boolean reflection helper. Returns true iff A is envy-free under valuation v.

Equations

• SocialChoice.FairDivision.Indivisible.isEnvyFree v A = decide (∀ (i j : N), v.val i (A j) ≤ v.val i (A i))

theorem SocialChoice.FairDivision.Indivisible.isEnvyFree_iff {N : Type u_1} {G : Type u_2} [Fintype N] (v : Valuation N G) (A : Allocation N G) : isEnvyFree v A = true ↔ IsEnvyFree v A

The envy-free checker is sound and complete.

EF1 reflection

noncomputable def SocialChoice.FairDivision.Indivisible.isEF1 {N : Type u_1} {G : Type u_2} [Fintype N] [DecidableEq N] [DecidableEq G] (v : Valuation N G) (A : Allocation N G) : Bool

Noncomputable EF1 Boolean reflection helper. Returns true iff A is envy-free up to one good under valuation v.

Equations

• SocialChoice.FairDivision.Indivisible.isEF1 v A = decide (∀ (i j : N), i ≠ j → (A j).Nonempty → ∃ g ∈ A j, v.val i (A j \ {g}) ≤ v.val i (A i))

theorem SocialChoice.FairDivision.Indivisible.isEF1_iff {N : Type u_1} {G : Type u_2} [Fintype N] [DecidableEq N] [DecidableEq G] (v : Valuation N G) (A : Allocation N G) : isEF1 v A = true ↔ IsEF1 v A

The EF1 checker is sound and complete.

EFX reflection

noncomputable def SocialChoice.FairDivision.Indivisible.isEFX {N : Type u_1} {G : Type u_2} [Fintype N] [DecidableEq N] [DecidableEq G] (v : Valuation N G) (A : Allocation N G) : Bool

Noncomputable EFX Boolean reflection helper. Returns true iff A is envy-free up to any good under valuation v.

Equations

• SocialChoice.FairDivision.Indivisible.isEFX v A = decide (∀ (i j : N), i ≠ j → ∀ g ∈ A j, v.val i (A j \ {g}) ≤ v.val i (A i))

theorem SocialChoice.FairDivision.Indivisible.isEFX_iff {N : Type u_1} {G : Type u_2} [Fintype N] [DecidableEq N] [DecidableEq G] (v : Valuation N G) (A : Allocation N G) : isEFX v A = true ↔ IsEFX v A

The EFX checker is sound and complete.

Proportionality reflection

noncomputable def SocialChoice.FairDivision.Indivisible.isProportional {N : Type u_1} {G : Type u_2} [Fintype N] (n : ℕ) (v : Valuation N G) (allGoods : Finset G) (A : Allocation N G) : Bool

Noncomputable proportionality Boolean reflection helper for n agents. Returns true iff every agent's bundle value is ≥ 1/n of the total.

The value codomain is fixed to ℝ, so this is noncomputable.

Equations

• SocialChoice.FairDivision.Indivisible.isProportional n v allGoods A = decide (∀ (i : N), v.val i allGoods ≤ ↑n * v.val i (A i))

theorem SocialChoice.FairDivision.Indivisible.isProportional_iff {N : Type u_1} {G : Type u_2} [Fintype N] (n : ℕ) (v : Valuation N G) (allGoods : Finset G) (A : Allocation N G) : isProportional n v allGoods A = true ↔ IsProportional n v allGoods A

The proportionality checker is sound and complete.