Perhaps the time is ripe to try to underpin these insights with some solid inferential foundation. Recall that we want to establish identity d = f , given *Definition 1* d(P) == d(x, y) denotes length in steps of minimal knight's move path connecting endpoints O = [0, 0] to P = [x, y] . *Definition 2* f(P) == f(x, y) := 3 if [X, Y] = [1, 0] , := 4 if [X, Y] = [2, 2] , := p - 2*Floor(q/r) otherwise; where [X, Y] := [|x|, |y|] if |x| >= |y| , := [|y|, |x|] otherwise; p := X-Y; q := p-Y; r := 3 if q < 0 , := 4 otherwise. Identity d = f would follow easily by induction from d(0, 0) = f(0, 0) , together with f(x, y) = 1 + min( f(x-2, y-1), ..., f(x+2, y+1) ) for [x, y] <> [0, 0] ; so denote h(x, y) == f(x, y) - 1 - min( f(x-2, y-1), ..., f(x+2, y+1) ) . Behold ... *Theorem* h(x, y) = 0 unless [x, y] = [0, 0] . Proof: Let P = [x, y] , P' = [x', y'] = [x-24, y-12] . Radii from origin through unit knight moves divide the plane into 8 sectors. Provided P, P' and their (knight's move) neighbours lie in corresponding sectors, the sign of q and residues (mod r) are same for both; then h(P) = h(P') . Via symmetry can assume P in octant x >= y >= 0 ; further consider region m == max(X, Y) > b , for constant b fixed as follows. We require that (1) P, P' and all their neighbours avoid special values of f(x, y) ; needs b-24-2 >= 2 , b >= 28 . (2) If P etc. occupy `rook' sector x > 2 |y| then so do P' etc; worst case P = (b, 0) needs b-24-1 + 2(-12-2) >= 0 , b >= 53 . (3) If P etc. occupy `bishop' sector |y|/2 < x < 2 y then so do P' etc; worst case P = (b, b) needs 2(b-24-2) - (b-12+1) >= 0 , b >= 41 . (4) If P etc. overlap radius x = 2 y then P' etc. must avoid radii 2 x = y and x = -2 y ; consequence of (2) & (3). Finally *** b = 53 *** suffices! Now to establish h(x, y) = 0 , settle initial cases m <= b via computation, then proceed via induction for m > b . Note P' may lie outside octant x >= y >= 0 ; the induction proceeds since via symmetry the result for bounded octant immediately implies the result for all P bounded by m . QED This has got legs. Does it stand up? Fred Lunnon On 4/9/14, Warren D Smith <warren.wds@gmail.com> wrote:
Lunnon questioning WDS: As I understand this, you want to enumerate all possible combinations of rounding after division by r = 3 or 4 following branch on sign(q); so where does your bound max(|x|, |y|) < 2999999 come from?
--it was to provide enough safety. My idea was to use brute force to avoid thinking. Since thinking clearly does not work well :)
You must ensure f(x, y) > 4 to avoid tangling with special values; given that, the rounding behaviour of your g simply repeats as |x|, |y| repeat modulo 12 . So it seems to me that you need only check f(x, y) = 1 + min( f(x-2, y-1), ..., f(x+2, y+1) ) in (one octant of) region max(|x|, |y|) <= 16 !
--maybe but I'm skeptical. I needed to work mod 24. Maybe mod 12 will do, but I played it safe. Anyhow, that indicates brute force confirmation region must extend at least 24*(something decently large) to make sure of self. Similarly the boundary regions I used on my cases were 50-wide to avoid worries re 24, etc etc. Again suggesting you better brute force it substantially further than 50. To be ultra sure I multiplied 50*24*24*3*SafetyFactor to get 2999999 as bound delineating brute force region which definitely should be safe.
I'm sure one could avoid a lot of this brute force, but the more you avoid, the more likely you'll go wrong.
On 4/9/14, Fred Lunnon <fred.lunnon@gmail.com> wrote:
As I understand this, you want to enumerate all possible combinations of rounding after division by r = 3 or 4 following branch on sign(q); so where does your bound max(|x|, |y|) < 2999999 come from?
You must ensure f(x, y) > 4 to avoid tangling with special values; given that, the rounding behaviour of your g simply repeats as |x|, |y| repeat modulo 12 . So it seems to me that you need only check f(x, y) = 1 + min( f(x-2, y-1), ..., f(x+2, y+1) ) in (one octant of) region max(|x|, |y|) <= 16 !
A trivial induction on d then completes the proof [I think -- but I've been wrong before].
Fred Lunnon
On 4/9/14, Warren D Smith <warren.wds@gmail.com> wrote:
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)
_______________________________________________ math-fun mailing list math-fun@mailman.xmission.com http://mailman.xmission.com/cgi-bin/mailman/listinfo/math-fun