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
• Election.quota
• 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, without anonymity (or any other property).

References

• M. L. Balinski, H. P. Young, Fair Representation: Meeting the Ideal of One Man, One Vote
• P. Gölz, D. Peters, A. D. Procaccia, In This Apportionment Lottery, the House Always Wins
• 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 and the total number of seats to be allocated.

• votes : Vector ℕ n

  The number of votes cast for each of the n parties, at the corresponding index.

• houseSize : ℕ+

  The number of seats to be allocated between the parties.

• votes_sum_pos : 0 < self.votes.sum

  At least one vote is cast, so that the standard quotas are well defined.

@[instance_reducible]

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.

@[instance_reducible]

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

Equations

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

def Apportionmentlib.«termElection![_;[_,,]]» : Lean.ParserDescr

Notation for an election with a literal house size and vote distribution, as in election![8; [66, 67, 245, 622]].

Equations

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

def Apportionmentlib.Election.quota {n : ℕ} (e : Election n) (i : Fin n) : ℚ

Party i's standard (Hare) quota: its proportional share of the house size.

Equations

• e.quota i = ↑e.votes[i] * ↑↑e.houseSize / ↑e.votes.sum

@[instance_reducible]

instance Apportionmentlib.instHtmlEvalElection {n : ℕ} : ProofWidgets.HtmlEval (Election n)

This instance enables rendering of elections using the #html command. For example,

#html election![8; [66, 67, 245, 622]]

Equations

• Apportionmentlib.instHtmlEvalElection = { eval := fun (e : Apportionmentlib.Election n) => pure (Apportionmentlib.Election.toHtml✝ e) }

def Apportionmentlib.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 Apportionmentlib.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 Apportionmentlib.Election.n_pos {n : ℕ} (election : Election n) : 0 < n

The number of parties in an election is positive.

@[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

@[instance_reducible]

instance Apportionmentlib.instReprApportionment {n : ℕ} : Repr (Apportionment n)

Equations

• Apportionmentlib.instReprApportionment = { reprPrec := fun (e : Apportionmentlib.Apportionment n) (x : ℕ) => Std.Format.text "#v" ++ repr (Vector.toList e) }

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)

  The set of apportionments that the rule returns for a given election.

• 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' := election.mkByPerm σ; ∀ (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' := election.mkByScale k; 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) (hApp : App ∈ rule.res election) : let election' := { votes := App, houseSize := election.houseSize, votes_sum_pos := ⋯ }; 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) (App : Apportionment n) : App ∈ rule.res election → ↑App[i] = ⌊election.quota i⌋ ∨ ↑App[i] = ⌈election.quota i⌉

theorem Apportionmentlib.Rule.seats_le (rule : Rule) [h_quota : IsQuotaRule rule] {n : ℕ} (election : Election n) (i : Fin n) (m : ℕ) (h : election.quota i ≤ ↑m) (App : Apportionment n) : App ∈ rule.res election → App[i] ≤ m

A quota rule allocates at most m seats to party i whenever its quota is at most m.

theorem Apportionmentlib.Rule.le_seats (rule : Rule) [h_quota : IsQuotaRule rule] {n : ℕ} (election : Election n) (i : Fin n) (m : ℕ) (h : ↑m ≤ election.quota i) (App : Apportionment n) : App ∈ rule.res election → m ≤ App[i]

A quota rule allocates at least m seats to party i whenever its quota is at least m.

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) [IsQuotaRule rule] : ¬IsPopulationMonotone rule

Balinski-Young impossibility theorem: a quota rule is never population monotone, so no apportionment method can satisfy both properties simultaneously. Anonymity is not assumed (nor any other property).

Gölz, Peters and Procaccia [GPP25] prove this for five or more parties, leaving four open in this generality; the witness used here has only four parties, settling that case.