Basic

We define basic notions related to apportionment methods, such as elections, apportionments, apportionment rules, and properties of apportionment rules. We also prove the Balinski-Young impossibility theorem.

All definitions follow those given in a textbook by F. Pukelsheim [Pukelsheim2017]. Distinction between weak and strong exactness is added, following [PalomaresPukelsheimRamirez2016].

Main definitions

• Election
• Apportionment
• Rule
• IsAnonymous
• IsBalanced
• IsConcordant
• IsDecent
• IsExact
• IsQuotaRule
• IsPopulationMonotone

Main statements

• Election.n_pos: the number of parties in an election is positive.
• IsConcordant_of_IsPopulationMonotone: anonymity and population monotonicity imply concordance.
• balinski_young: Balinski-Young impossibility theorem.

References

• [M. L. Balinski, H. P. Young, Fair Representation: Meeting the Ideal of One Man, One Vote ][BalinskiYoung1982]
• [A. Palomares, F. Pukelsheim, J. A. Ramírez, The whole and its parts: On the coherence theorem of Balinski and Young][PalomaresPukelsheimRamirez2016]
• [F. Pukelsheim, Proportional Representation: Apportionment Methods and Their Applications ][Pukelsheim2017]

@[reducible, inline]

abbrev Apportionment (n : ℕ) : Type

An apportionment is a vector of natural numbers representing the number of seats allocated to each party (at the corresponding index).

Equations

• Apportionment n = Vector ℕ n

structure Apportionment.Election (n : ℕ) : Type

An election with a vector of votes for n parties (at the corresponding indices) and the total number of seats to be allocated.

• votes : Vector ℕ n

  The number of votes for each of the n parties.

• houseSize : ℕ+

  The total number of seats to be allocated.

• votes_sum_pos : 0 < self.votes.sum

  At least one party must have received some votes.

def Apportionment.instDecidableEqElection.decEq {n✝ : ℕ} (x✝ x✝¹ : Election n✝) : Decidable (x✝ = x✝¹)

Equations

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

@[implicit_reducible]

instance Apportionment.instDecidableEqElection {n✝ : ℕ} : DecidableEq (Election n✝)

Equations

• Apportionment.instDecidableEqElection = Apportionment.instDecidableEqElection.decEq

@[implicit_reducible]

instance Apportionment.instReprElection {n : ℕ} : Repr (Election n)

Equations

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

def Apportionment.Election.mkByPerm {n : ℕ} (election : Election n) (σ : Equiv.Perm (Fin n)) : Election n

Create a new election by permuting the vote distribution of parties according to permutation σ.

Equations

• election.mkByPerm σ = { votes := Vector.ofFn fun (i : Fin n) => election.votes[σ i], houseSize := election.houseSize, votes_sum_pos := ⋯ }

def Apportionment.Election.mkByScale {n : ℕ} (election : Election n) (k : ℕ+) : Election n

Create a new election by scaling all votes by a positive constant k.

Equations

• election.mkByScale k = { votes := Vector.ofFn fun (i : Fin n) => ↑k * election.votes[i], houseSize := election.houseSize, votes_sum_pos := ⋯ }

theorem Apportionment.Election.n_pos {n : ℕ} (election : Election n) : 0 < n

The number of parties in an election is positive.

structure Apportionment.Rule : Type

An apportionment rule is a function that, given an election, returns a set of apportionments satisfying three properties:

1. Non-emptiness: there is at least one apportionment returned;
2. Inheritance of zeros: parties with zero votes are allocated zero seats;
3. House size feasibility: the total number of seats allocated is equal to the house size.

• res {n : ℕ} : Election n → Finset (Apportionment n)

  The set of apportionments produced for a given election.

• non_emptiness {n : ℕ} (election : Election n) : (self.res election).Nonempty

  Every election produces at least one apportionment.

• inheritance_of_zeros {n : ℕ} (election : Election n) (i : Fin n) : election.votes[i] = 0 → ∀ App ∈ self.res election, App[i] = 0

  Parties with zero votes receive zero seats.

• house_size_feasibility {n : ℕ} (election : Election n) (App : Apportionment n) : App ∈ self.res election → Vector.sum App = ↑election.houseSize

  The total number of seats allocated equals the house size.

class Apportionment.IsAnonymous (rule : Rule) : Prop

A rule is anonymous if permuting the votes of the parties permutes the allocation of seats in the same way.

• anonymous {n : ℕ} (election : Election n) (σ : Equiv.Perm (Fin n)) : let election' := election.mkByPerm σ; ∀ (App : Apportionment n), App ∈ rule.res election' ↔ ∃ App' ∈ rule.res election, ∀ (i : Fin n), App[i] = App'[σ i]

  Permuting the votes by σ permutes the resulting apportionments by σ.

class Apportionment.IsBalanced (rule : Rule) : Prop

A rule is balanced if whenever two parties have the same number of votes, then the difference in the number of seats allocated to them is at most one.

• balanced {n : ℕ} (election : Election n) (i j : Fin n) : election.votes[i] = election.votes[j] → ∀ App ∈ rule.res election, App[i].dist App[j] ≤ 1

  Equal vote counts produce seat counts that differ by at most one.

class Apportionment.IsConcordant (rule : Rule) : Prop

A rule is concordant if whenever one party has fewer votes than another, then it is allocated no more seats than that other party.

• concordant {n : ℕ} (election : Election n) (i j : Fin n) : election.votes[i] < election.votes[j] → ∀ App ∈ rule.res election, App[i] ≤ App[j]

  Strictly fewer votes implies no more seats.

class Apportionment.IsDecent (rule : Rule) : Prop

A rule is decent if scaling the number of votes for each party by the same positive integer does not change the apportionment.

• decent {n : ℕ} (election : Election n) (k : ℕ+) : let election' := election.mkByScale k; rule.res election' = rule.res election

  Scaling all vote counts by a positive integer leaves the apportionment unchanged.

class Apportionment.IsExact (rule : Rule) : Prop

A rule is weakly exact if every Apportionment, when viewed as an input vote distribution Election.votes, is reproduced as the unique solution.

• exact {n : ℕ} (election : Election n) (App : Apportionment n) (hApp : App ∈ rule.res election) : let election' := { votes := App, houseSize := election.houseSize, votes_sum_pos := ⋯ }; rule.res election' = {App}

  An apportionment, treated as a vote distribution, is the unique apportionment of itself.

class Apportionment.IsQuotaRule (rule : Rule) : Prop

A rule is a quota rule if the number of seats allocated to each party is either the floor or the ceiling of its Hare-quota.

• quota_rule {n : ℕ} (election : Election n) (i : Fin n) : let quota := ↑election.votes[i] * ↑↑election.houseSize / ↑election.votes.sum; ∀ App ∈ rule.res election, ↑App[i] = ⌊quota⌋ ∨ ↑App[i] = ⌈quota⌉

  Each party receives the floor or ceiling of its Hare-quota.

class Apportionment.IsPopulationMonotone (rule : Rule) : Prop

A rule is population monotone (or vote ratio monotone) if population paradoxes do not occur. A population paradox occurs when the support for party i increases at a faster rate than that for party j, but i loses seats while j gains seats.

• population_monotone {n : ℕ} (election₁ election₂ : Election n) (i j : Fin n) : election₁.houseSize = election₂.houseSize → election₂.votes[i] * election₁.votes[j] > election₂.votes[j] * election₁.votes[i] → ∀ App₁ ∈ rule.res election₁, ∀ App₂ ∈ rule.res election₂, ¬(App₁[i] > App₂[i] ∧ App₁[j] < App₂[j])

  Faster vote growth for i than for j rules out i losing seats while j gains them.

theorem Apportionment.IsConcordant_of_IsPopulationMonotone (rule : Rule) [h_anon : IsAnonymous rule] [h_mono : IsPopulationMonotone rule] : IsConcordant rule

If an anonymous rule is population monotone, then it is concordant.

theorem Apportionment.balinski_young (rule : Rule) [IsAnonymous rule] [h_quota : IsQuotaRule rule] : ¬IsPopulationMonotone rule

Balinski-Young impossibility theorem: If an anonymous rule is a quota rule, then it is not population monotone. Thus, no apportionment method can satisfy both properties simultaneously.