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

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

Main statements

• if_IsPopulationMonotone_then_IsConcordant: anonymity and population monotonicity imply concordance.
• balinski_young: Balinski-Young impossibility theorem.

Implementation details

Formally, we should use p ∈ election.parties everywhere, in addition to simply writing p : Party, in the definitions of IsAnonymous, IsPopulationMonotone, etc. We omit this for simplicity, as for now, since it has not been needed in any proof so far. This is not surprising, as we define Election.votes with | _ => 0, so parties outside election.parties have no votes.

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 Party : Type

Party (or candidate, state, etc.) in an election. They are identified by their name.

• name : String

instance instDecidableEqParty : DecidableEq Party

Equations

• instDecidableEqParty = instDecidableEqParty.decEq

def instDecidableEqParty.decEq (x✝ x✝¹ : Party) : Decidable (x✝ = x✝¹)

Equations

• instDecidableEqParty.decEq { name := a } { name := b } = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯

instance instReprParty : Repr Party

Equations

• instReprParty = { reprPrec := fun (p : Party) (x : ℕ) => Std.Format.text (toString p.name ++ toString " : Party") }

structure Election : Type

An election with a finite set of parties, a function giving the number of votes for each party, and the total number of seats to be allocated.

• parties : Finset Party
• votes : Party → ℕ
• house_size : ℕ

def Election.total_voters (election : Election) : ℕ

Equations

• election.total_voters = ∑ p ∈ election.parties, election.votes p

@[reducible, inline]

abbrev Apportionment : Type

An apportionment is a function from parties to the number of seats allocated to each party.

Equations

• Apportionment = (Party → ℕ)

structure 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 : Election → Finset Apportionment
• non_emptiness (election : Election) : (self.res election).Nonempty
• inheritance_of_zeros (election : Election) (p : Party) : election.votes p = 0 → ∀ App ∈ self.res election, App p = 0
• house_size_feasibility (election : Election) (App : Apportionment) : App ∈ self.res election → ∑ p ∈ election.parties, App p = election.house_size

class IsAnonymous [Fintype Party] (rule : Rule) : Prop

A rule is anonymous if permuting the votes of the parties permutes the allocation of seats in the same way. Informally, the names of the parties do not matter.

• anonymous (election : Election) (σ : Party → Party) (p q : Party) : (σ p = σ q → p = q) → let election' := { parties := election.parties, votes := election.votes ∘ σ, house_size := election.house_size }; rule.res election' = Finset.image (fun (x : Party → ℕ) => x ∘ σ) (rule.res election)

class IsBalanced (rule : Rule) : Prop

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

• balanced (election : Election) (p q : Party) : election.votes p = election.votes q → ∀ App ∈ rule.res election, (App p).dist (App q) ≤ 1

class IsConcordant (rule : Rule) : Prop

A rule is concordant if whenever party p has fewer votes than party q, then p is allocated no more seats than q.

• concordant (election : Election) (p q : Party) : election.votes p < election.votes q → ∀ App ∈ rule.res election, App p ≤ App q

class IsDecent (rule : Rule) : Prop

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

• decent (election : Election) (k : ℕ+) : let election' := { parties := election.parties, votes := fun (p : Party) => ↑k * election.votes p, house_size := election.house_size }; rule.res election' = rule.res election

class 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 (election : Election) (App : Apportionment) : App ∈ rule.res election → let election' := { parties := election.parties, votes := App, house_size := election.house_size }; rule.res election' = {App}

class IsQuotaRule (rule : Rule) : Prop

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

• quota_rule (election : Election) (p : Party) : let quota := ↑(election.votes p) * ↑election.house_size / ↑election.total_voters; ∀ App ∈ rule.res election, ↑(App p) = ⌊quota⌋ ∨ ↑(App p) = ⌈quota⌉

class 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 p increases at a faster rate than that for party q, but p loses seats while q gains seats.

• population_monotonone (election₁ election₂ : Election) (p q : Party) : election₁.parties = election₂.parties ∧ election₁.house_size = election₂.house_size → election₂.votes p * election₁.votes q > election₂.votes q * election₁.votes p → ∀ App₁ ∈ rule.res election₁, ∀ App₂ ∈ rule.res election₂, ¬(App₁ p > App₂ p ∧ App₁ q < App₂ q)

theorem if_IsPopulationMonotone_then_IsConcordant [Fintype Party] (rule : Rule) [h_anon : IsAnonymous rule] [h_mono : IsPopulationMonotone rule] : IsConcordant rule

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

theorem balinski_young [Fintype Party] (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.