I think the argument below (admittedly sketchy) now proves it. 1. Recall the problem comes down to proving that g(x,y)=1 for all x,y except x=y=0, and g(0,0)=-1. Here g(x,y) is a certain known formula I stated in an earlier post. 2. Computer verifies that for all x,y with max(|x|,|y|)<2999999. This should require less than a day of computing. I'd already done it up to 20000. 3. Divide into the following cases: Case1[k,v,w]: k<=y, y+k<=x, x mod 24=v, y mod 24=w Case2[k,v,w]: 0<=y<k, y+k<=x, x mod 24=v, y mod 24=w Case3[k,v,w]: k<=y<=x<y+k, x mod 24=v, y mod 24=w Here k can be anywhere from 0 to 49, and v and w each anywhere in {0,1,...,23}, so this is 86400=3*50*24*24 cases in all. 4. Within each of the above cases, the formula for g(x,y) simplifies. Specifically, all the floor functions can be removed since floor(linear polynomial) in each of these cases just becomes (the polynomial plus a known constant). All polynomials have all coefficients equal to integers divided by 24. Further, the max and min functions inside the formula also can be removed since in each case it can be deduced a priori which argument of the min or max is the one that wins. 5. We do not actually need to do any of that simplifying ourselves(!) -- we merely need to know that it could in principle be done. Because of this combined with the fact verification worked in step (2) we can deduce from (4) that the polynomials must in fact simplify, in every single case, to: 1. If even one did not, the computer would have detected that in step (2). 6. Theorem proven. -- Warren D. Smith http://RangeVoting.org <-- add your endorsement (by clicking "endorse" as 1st step)