[EM] Another interesting property of the unfortunates class of method

[Kristofer Munsterhjelm]

What I mean by the "unfortunates class" is a Droop-proportional method 
like this:
	1. Use an appropriate method to elect n-1 of n
	2. Eliminate the loser and repeat until n-1 is equal to the number of 
seats you want.

I just realized that this class of method is house-monotone! Because 
we're eliminating down to a given size set, the result for a smaller 
election must be a subset of the result for a larger election.

In other words: nobody gets kicked out when going from a smaller seat 
outcome to a larger seat outcome. So for all its flaws, this does show 
that house monotonicity and Droop proportionality are compatible! I 
wouldn't have thought that's possible.

There's a disadvantage, though. It means that *every* unfortunates-class 
method has center squeeze in it, for the same reason that the Bucklin 
method I described does. So these would all make pretty awful 
single-winner methods.

And probably, by analogy to the difference between unconstrained and 
hierarchical clustering, one can show that a good non-house monotone 
method can produce much better results than the best house monotone method.

But still: I didn't know that was possible. I knew it was possible for 
party list, but it's the kind of thing I thought couldn't possibly hold 
for more complex ranked ballots.

On another note: I've been tinkering with Z3 and I *think* it says that 
there exists no single vector v so that:
	(fpB > 1/3 and fpC > 1/3 > 0) or
	(lpA > 2/3) implies

	v dot [A>B A>C B>C |V|] > 0
		(i.e. "the loser according to v is A")

and
	when rotating the candidates, there's never a situation where
		the loser according to v is more than one candidate.

I.e. there's no way to, with a single vector, use pairwise counts alone 
to create a method that ejects unfortunates and never says that two 
candidates both lose.

Baby steps, but still... I suspect it's true in general: that pairwise 
counts can't be used to discern such positionally based conditions.

-km