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 [Puk17]. Distinction between weak and strong exactness is added, following [PPR16].

Main definitions

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

Main statements

• 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
• A. Palomares, F. Pukelsheim, J. A. Ramírez, The whole and its parts: On the coherence theorem of Balinski and Young
• F. Pukelsheim, Proportional Representation: Apportionment Methods and Their Applications

structure Apportionmentlib.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
• houseSize : ℕ

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

Equations

• Apportionmentlib.instDecidableEqElection = Apportionmentlib.instDecidableEqElection.decEq

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

Equations

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

@[reducible, inline]

abbrev Apportionmentlib.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

• Apportionmentlib.Apportionment n = Vector ℕ n

structure Apportionmentlib.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)
• non_emptiness {n : ℕ} (election : Election n) : (self.res election).Nonempty
• inheritance_of_zeros {n : ℕ} (election : Election n) (i : Fin n) : election.votes[i] = 0 → ∀ App ∈ self.res election, App[i] = 0
• house_size_feasibility {n : ℕ} (election : Election n) (App : Apportionment n) : App ∈ self.res election → Vector.sum App = election.houseSize

class Apportionmentlib.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' := { votes := Vector.ofFn fun (i : Fin n) => election.votes[σ i], houseSize := election.houseSize }; ∀ (App : Apportionment n), App ∈ rule.res election' ↔ ∃ App' ∈ rule.res election, ∀ (i : Fin n), App[i] = App'[σ i]

class Apportionmentlib.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

class Apportionmentlib.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]

class Apportionmentlib.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' := { votes := Vector.ofFn fun (i : Fin n) => ↑k * election.votes[i], houseSize := election.houseSize }; rule.res election' = rule.res election

class Apportionmentlib.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) : App ∈ rule.res election → let election' := { votes := App, houseSize := election.houseSize }; rule.res election' = {App}

class Apportionmentlib.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⌉

class Apportionmentlib.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])

theorem Apportionmentlib.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 Apportionmentlib.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.