[EM] Possible monotone resistant method?

[Kristofer Munsterhjelm]

I might have found a way to get monotonicity too. If so, that would be a 
first, even though the construction cheats a bit by violating 
unrestricted domain.

The proof below aims to show that if a method passes strong monotonicity 
in the sense I used in the post about cloneproofing, then the 
no-disqualification elimination method I gave there, with the social 
order of that method as its "external social order", is monotone.

Then all I have to do is use Range as the base method, since it passes 
strong monotonicity. While the UD failure from using rated ballots is a 
bit of a bummer, I think this is interesting because it shows that 
electing from the resistant set is not inherently incompatible with 
monotonicity. It's possible that the unusually demanding strong 
monotonicity constraint can be relaxed later.

Or to put it another way, by managing to prove something under very 
forgiving conditions, it shows that what I'm trying to do is not 
outright impossible.

Anyway.

Proof by induction over the external social order. I'll add candidates 
to the bottom end of the social order as the inductive step.

The base step with two candidates: Suppose that A uniquely wins. If the 
social order is A>B, raising A can't do anything to it, and can only 
establish A ~> B if it's not already established. Neither of these can 
harm A, so A will still win.
If the social order is B>A, then A wins because A ~> B (otherwise A 
would be the lowest ranked non-disqualifying candidate and would be 
eliminated). Raising A can only change the social order to A>B which 
would again have no effect.
If B wins, then we can't do worse than A losing, so raising A can never 
violate monotonicity. For lowering A leading to B winning, just flip A 
and B's names.

So now suppose that every election with n candidates exhibits 
monotonicity, and we want to show it for (n+1) candidates. The idea is 
that after some candidate has been eliminated, we're back to the 
n-candidate case, so if we can do the induction step properly, then 
everything is fine.

So suppose we have an (n+1)-candidate election where A wins, and 
Y_before is the candidate who will first be eliminated. Clearly A wins 
when starting from the n-candidate election after Y_before has been 
eliminated, and by the inductive hypothesis this n-candidate election 
passes mono-raise (as every n-candidate election where A wins does; and 
by neutrality, as every n-candidate election does). It is also obvious 
that Y_before is not A, or A couldn't have won.

Let Y_after be the candidate who is first eliminated after raising A.

If we can show Y_before = Y_after, then monotonicity follows, because 
the same candidate will be eliminated and we reduce to an n-candidate 
election that we know A is going to win, by the inductive hypothesis.

When we raise A, the following may happen:
	- A is moved closer to the top of the social ordering
	- A ~> B is established for some other B.

In particular, it's not possible for B ~> C to be affected, a new 
disqualification B ~> A to be established, or the relative order of B 
and C to change in the social order, for any B and C. (The latter is by 
strong monotonicity of the base method.)

Consider the filtered social order, which is the social order after 
every candidate who is disqualifying someone else is removed. The 
elimination step eliminates the lowest ranked candidate in this filtered 
order. That can't be A because Y_before isn't A and the base method 
passes monotonicity. Raising A can't establish Y_before ~> X for any X, 
so Y_before is still on the filtered ranking. And by strong 
monotonicity, he must still be last.

Hence Y_after = Y_before as desired.

I haven't dealt with ties (which going by IRV, can be a problem for 
elimination methods), so I'll just take the mathematically cheap Ranked 
Pairs way out: break ties in the social order by random voter hierarchy. 
Now A always uniquely wins or loses (for any given choice of the RVH 
tiebreak). This is a bit of a hack, but we are dealing with a proof of 
concept.

Does that sound right?

-km