EconCSLib.SocialChoice.Voting.Basic

Voting-specific social-choice infrastructure: finite strict preference profiles, set-valued voting rules, social welfare functions, and the core voting axioms.

The foundation-level Pref bundle is the library-wide weak-preference interface. The voting layer specializes to the standard ranked-ballot model: each voter submits a linear order over a finite set of alternatives, and a voting rule returns a finite set of winners.

Strict finite voting profiles

structure SocialChoice.Voting.Profile (N : Type u_3) (A : Type u_4) [Fintype N] [Fintype A] : Type (max u_3 u_4)

A voting profile assigns each voter a strict linear order over alternatives.

• pref : N → LinearOrder A

  The ballot submitted by each voter. Smaller means more preferred.

def SocialChoice.Voting.constantProfile {N : Type u_1} {A : Type u_2} [Fintype N] [Fintype A] (r : LinearOrder A) : Profile N A

Constant profile where every voter submits the same ballot.

Equations

• SocialChoice.Voting.constantProfile r = { pref := fun (x : N) => r }

theorem SocialChoice.Voting.Profile.ext {N : Type u_1} {A : Type u_2} [Fintype N] [Fintype A] {P Q : Profile N A} (h : ∀ (i : N), P.pref i = Q.pref i) : P = Q

theorem SocialChoice.Voting.Profile.ext_iff {N : Type u_1} {A : Type u_2} [Fintype N] [Fintype A] {P Q : Profile N A} : P = Q ↔ ∀ (i : N), P.pref i = Q.pref i

@[reducible, inline]

abbrev SocialChoice.Voting.ballotLE {A : Type u_2} (r : LinearOrder A) : LE A

Ballot r ranks a strictly above b.

Equations

• SocialChoice.Voting.ballotLE r = r.toLE

@[reducible, inline]

abbrev SocialChoice.Voting.ballotLT {A : Type u_2} (r : LinearOrder A) : LT A

Ballot r's strict-order instance, exposed explicitly to avoid ambient typeclass search.

Equations

• SocialChoice.Voting.ballotLT r = r.toLT

def SocialChoice.Voting.BallotPrefers {A : Type u_2} (r : LinearOrder A) (a b : A) : Prop

Ballot r ranks a strictly above b.

Equations

• SocialChoice.Voting.BallotPrefers r a b = (a < b)

noncomputable def SocialChoice.Voting.ballotFromInjective {A : Type u_2} {B : Type u_3} (rB : LinearOrder B) (f : A → B) (hf : Function.Injective f) : LinearOrder A

Pull a linear order back along an injective map, using the supplied codomain order explicitly rather than relying on ambient typeclass search. This is the safe constructor for ballots on types such as Fin n, which already carry a default order.

Equations

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

@[simp]

theorem SocialChoice.Voting.BallotPrefers_ballotFromInjective {A : Type u_2} {B : Type u_3} (rB : LinearOrder B) (f : A → B) (hf : Function.Injective f) (a b : A) : BallotPrefers (ballotFromInjective rB f hf) a b ↔ f a < f b

theorem SocialChoice.Voting.BallotPrefers.asymm {A : Type u_2} (r : LinearOrder A) {a b : A} : BallotPrefers r a b → ¬BallotPrefers r b a

theorem SocialChoice.Voting.BallotPrefers.total_of_ne {A : Type u_2} (r : LinearOrder A) {a b : A} (hne : a ≠ b) : BallotPrefers r a b ∨ BallotPrefers r b a

def SocialChoice.Voting.Prefers {N : Type u_1} {A : Type u_2} [Fintype N] [Fintype A] (P : Profile N A) (i : N) (a b : A) : Prop

Voter i strictly prefers a to b in profile P.

Equations

• SocialChoice.Voting.Prefers P i a b = SocialChoice.Voting.BallotPrefers (P.pref i) a b

theorem SocialChoice.Voting.Prefers.asymm {N : Type u_1} {A : Type u_2} [Fintype N] [Fintype A] (P : Profile N A) (i : N) {a b : A} : Prefers P i a b → ¬Prefers P i b a

theorem SocialChoice.Voting.Prefers.total_of_ne {N : Type u_1} {A : Type u_2} [Fintype N] [Fintype A] (P : Profile N A) (i : N) {a b : A} (hne : a ≠ b) : Prefers P i a b ∨ Prefers P i b a

def SocialChoice.Voting.TopRank {N : Type u_1} {A : Type u_2} [Fintype N] [Fintype A] (P : Profile N A) (i : N) (a : A) : Prop

Candidate a is top-ranked by voter i.

Equations

• SocialChoice.Voting.TopRank P i a = ∀ (b : A), b ≠ a → SocialChoice.Voting.Prefers P i a b

def SocialChoice.Voting.BottomRank {N : Type u_1} {A : Type u_2} [Fintype N] [Fintype A] (P : Profile N A) (i : N) (a : A) : Prop

Candidate a is bottom-ranked by voter i.

Equations

• SocialChoice.Voting.BottomRank P i a = ∀ (b : A), b ≠ a → SocialChoice.Voting.Prefers P i b a

def SocialChoice.Voting.BallotTop {A : Type u_2} (r : LinearOrder A) (a : A) : Prop

A linear-order ballot ranks a first.

Equations

• SocialChoice.Voting.BallotTop r a = ∀ (b : A), b ≠ a → SocialChoice.Voting.BallotPrefers r a b

def SocialChoice.Voting.BallotBottom {A : Type u_2} (r : LinearOrder A) (a : A) : Prop

A linear-order ballot ranks a last.

Equations

• SocialChoice.Voting.BallotBottom r a = ∀ (b : A), b ≠ a → SocialChoice.Voting.BallotPrefers r b a

noncomputable def SocialChoice.Voting.topChoice {N : Type u_1} {A : Type u_2} [Fintype N] [Fintype A] [Nonempty A] (P : Profile N A) (i : N) : A

The top-ranked alternative of voter i.

Equations

• SocialChoice.Voting.topChoice P i = Finset.univ.min' ⋯

theorem SocialChoice.Voting.topChoice_topRank {N : Type u_1} {A : Type u_2} [Fintype N] [Fintype A] [Nonempty A] (P : Profile N A) (i : N) : TopRank P i (topChoice P i)

theorem SocialChoice.Voting.topRank_eq_topChoice {N : Type u_1} {A : Type u_2} [Fintype N] [Fintype A] [Nonempty A] (P : Profile N A) (i : N) (a : A) (ha : TopRank P i a) : a = topChoice P i

Profile transformations

@[reducible]

noncomputable def SocialChoice.Voting.updateProfile {N : Type u_1} {A : Type u_2} [Fintype N] [Fintype A] (P : Profile N A) (i : N) (r : LinearOrder A) : Profile N A

Replace one voter's ballot.

Equations

• SocialChoice.Voting.updateProfile P i r = { pref := fun (j : N) => if j = i then r else P.pref j }

def SocialChoice.Voting.permuteVoters {N : Type u_1} {A : Type u_2} [Fintype N] [Fintype A] (P : Profile N A) (σ : Equiv.Perm N) : Profile N A

Relabel voters by a permutation of the electorate.

Equations

• SocialChoice.Voting.permuteVoters P σ = { pref := fun (i : N) => P.pref (σ i) }

noncomputable def SocialChoice.Voting.relabelBallot {A : Type u_2} (r : LinearOrder A) (σ : Equiv.Perm A) : LinearOrder A

Relabel a linear order along a permutation of alternatives.

Equations

• SocialChoice.Voting.relabelBallot r σ = SocialChoice.Voting.ballotFromInjective r ⇑σ ⋯

noncomputable def SocialChoice.Voting.relabelBallotEquiv {A : Type u_2} {B : Type u_3} (r : LinearOrder A) (e : A ≃ B) : LinearOrder B

Relabel a linear order along an equivalence of alternative types.

Equations

• SocialChoice.Voting.relabelBallotEquiv r e = SocialChoice.Voting.ballotFromInjective r ⇑e.symm ⋯

noncomputable def SocialChoice.Voting.permuteCandidates {N : Type u_1} {A : Type u_2} [Fintype N] [Fintype A] (P : Profile N A) (σ : Equiv.Perm A) : Profile N A

Relabel candidates by applying the inverse permutation to each ballot.

Equations

• SocialChoice.Voting.permuteCandidates P σ = { pref := fun (i : N) => SocialChoice.Voting.relabelBallot (P.pref i) (Equiv.symm σ) }

noncomputable def SocialChoice.Voting.relabelProfile {N : Type u_1} {A : Type u_2} {B : Type u_3} [Fintype N] [Fintype A] [Fintype B] (P : Profile N A) (e : A ≃ B) : Profile N B

Relabel a profile along an equivalence of alternative types.

Equations

• SocialChoice.Voting.relabelProfile P e = { pref := fun (i : N) => SocialChoice.Voting.relabelBallotEquiv (P.pref i) e }

Voting rules and social welfare functions

@[reducible, inline]

abbrev SocialChoice.Voting.VotingRule (N : Type u_3) (A : Type u_4) [Fintype N] [Fintype A] : Type (max u_4 u_3)

A set-valued voting rule on fixed finite voter and candidate types.

Equations

• SocialChoice.Voting.VotingRule N A = (SocialChoice.Voting.Profile N A → Finset A)

def SocialChoice.Voting.IsTotal {N : Type u_1} {A : Type u_2} [Fintype N] [Fintype A] (f : VotingRule N A) : Prop

A voting rule is total if it always returns at least one winner.

Equations

• SocialChoice.Voting.IsTotal f = ∀ (P : SocialChoice.Voting.Profile N A), (f P).Nonempty

def SocialChoice.Voting.Resolute {N : Type u_1} {A : Type u_2} [Fintype N] [Fintype A] (f : VotingRule N A) : Prop

A voting rule is resolute if it always returns exactly one winner.

Equations

• SocialChoice.Voting.Resolute f = ∀ (P : SocialChoice.Voting.Profile N A), (f P).card = 1

@[reducible, inline]

abbrev SocialChoice.Voting.SWF (N : Type u_3) (A : Type u_4) [Fintype N] [Fintype A] : Type (max u_4 u_3)

A social welfare function maps strict profiles to a weak social preference.

Equations

• SocialChoice.Voting.SWF N A = (SocialChoice.Voting.Profile N A → Pref A)

def SocialChoice.Voting.SWF.Unanimity {N : Type u_1} {A : Type u_2} [Fintype N] [Fintype A] (F : SWF N A) : Prop

Unanimity/Pareto for SWFs: unanimous strict preference forces social strict preference.

Equations

• F.Unanimity = ∀ (P : SocialChoice.Voting.Profile N A) (a b : A), (∀ (i : N), SocialChoice.Voting.Prefers P i a b) → strict (F P).rel a b

def SocialChoice.Voting.SWF.IIA {N : Type u_1} {A : Type u_2} [Fintype N] [Fintype A] (F : SWF N A) : Prop

Independence of irrelevant alternatives for SWFs.

Equations

• F.IIA = ∀ (P Q : SocialChoice.Voting.Profile N A) (a b : A), (∀ (i : N), SocialChoice.Voting.Prefers P i a b ↔ SocialChoice.Voting.Prefers Q i a b) → ((F P).rel a b ↔ (F Q).rel a b)

def SocialChoice.Voting.SWF.Dictatorial {N : Type u_1} {A : Type u_2} [Fintype N] [Fintype A] (F : SWF N A) : Prop

A SWF is dictatorial if one voter always determines every strict social comparison.

Equations

• F.Dictatorial = ∃ (i : N), ∀ (P : SocialChoice.Voting.Profile N A) (a b : A), SocialChoice.Voting.Prefers P i a b → strict (F P).rel a b

def SocialChoice.Voting.SWF.NonDictatorial {N : Type u_1} {A : Type u_2} [Fintype N] [Fintype A] (F : SWF N A) : Prop

A SWF is non-dictatorial.

Equations

• F.NonDictatorial = ¬F.Dictatorial

Voting-rule axioms

def SocialChoice.Voting.Unanimity {N : Type u_1} {A : Type u_2} [Fintype N] [Fintype A] (f : VotingRule N A) : Prop

Unanimity/Pareto for set-valued voting rules: no unanimously dominated alternative is selected.

Equations

• SocialChoice.Voting.Unanimity f = ∀ (P : SocialChoice.Voting.Profile N A) (a b : A), (∀ (i : N), SocialChoice.Voting.Prefers P i a b) → b ∉ f P

@[reducible, inline]

abbrev SocialChoice.Voting.ParetoEfficiency {N : Type u_1} {A : Type u_2} [Fintype N] [Fintype A] (f : VotingRule N A) : Prop

Alias for voting-rule unanimity in its weak-Pareto form.

Equations

• SocialChoice.Voting.ParetoEfficiency f = SocialChoice.Voting.Unanimity f

theorem SocialChoice.Voting.top_unanimity_of_unanimity {N : Type u_1} {A : Type u_2} [Fintype N] [Fintype A] [Nonempty A] {f : VotingRule N A} (hf : IsTotal f) (hU : Unanimity f) (P : Profile N A) (a : A) : (∀ (i : N), TopRank P i a) → f P = {a}

Top unanimity follows from weak-Pareto unanimity plus totality: if every voter ranks a first, then a is the unique winner.

def SocialChoice.Voting.Anonymity {N : Type u_1} {A : Type u_2} [Fintype N] [Fintype A] (f : VotingRule N A) : Prop

Anonymity: relabeling voters does not change the winner set.

Equations

• SocialChoice.Voting.Anonymity f = ∀ (P : SocialChoice.Voting.Profile N A) (σ : Equiv.Perm N), f (SocialChoice.Voting.permuteVoters P σ) = f P

noncomputable def SocialChoice.Voting.permuteWinners {A : Type u_2} (σ : Equiv.Perm A) (s : Finset A) : Finset A

Candidate renaming on winner sets.

Equations

• SocialChoice.Voting.permuteWinners σ s = Finset.map (Equiv.toEmbedding σ) s

def SocialChoice.Voting.Neutrality {N : Type u_1} {A : Type u_2} [Fintype N] [Fintype A] (f : VotingRule N A) : Prop

Neutrality: relabeling candidates relabels the winner set.

Equations

• SocialChoice.Voting.Neutrality f = ∀ (P : SocialChoice.Voting.Profile N A) (σ : Equiv.Perm A), SocialChoice.Voting.permuteWinners σ (f P) = f (SocialChoice.Voting.permuteCandidates P σ)

def SocialChoice.Voting.SimpleLift {N : Type u_1} {A : Type u_2} [Fintype N] [Fintype A] (Q P : Profile N A) (a : A) : Prop

Q is obtained from P by weakly raising a: anything below a in P remains below a in Q, and anything above a in Q was already above a in P.

Equations

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

def SocialChoice.Voting.Monotonicity {N : Type u_1} {A : Type u_2} [Fintype N] [Fintype A] (f : VotingRule N A) : Prop

Monotonicity: raising a selected alternative cannot make it unselected.

Equations

• SocialChoice.Voting.Monotonicity f = ∀ (P Q : SocialChoice.Voting.Profile N A), ∀ a ∈ f P, SocialChoice.Voting.SimpleLift Q P a → a ∈ f Q

def SocialChoice.Voting.ResoluteStrategyproofness {N : Type u_1} {A : Type u_2} [Fintype N] [Fintype A] (f : VotingRule N A) (_hf : Resolute f) : Prop

Strategyproofness for resolute rules: changing one ballot cannot produce a strictly better unique winner for the deviating voter.

Equations

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

def SocialChoice.Voting.OptimistStrategyproofness {N : Type u_1} {A : Type u_2} [Fintype N] [Fintype A] (f : VotingRule N A) : Prop

Optimist strategyproofness for set-valued rules.

Equations

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

def SocialChoice.Voting.PessimistStrategyproofness {N : Type u_1} {A : Type u_2} [Fintype N] [Fintype A] (f : VotingRule N A) : Prop

Pessimist strategyproofness for set-valued rules.

Equations

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

def SocialChoice.Voting.Dictatorial {N : Type u_1} {A : Type u_2} [Fintype N] [Fintype A] [Nonempty A] (f : VotingRule N A) : Prop

A rule is dictatorial if one voter always gets their top-ranked alternative as the unique winner.

Equations

• SocialChoice.Voting.Dictatorial f = ∃ (i : N), ∀ (P : SocialChoice.Voting.Profile N A), f P = {SocialChoice.Voting.topChoice P i}