import java.applet.Applet;
import java.awt.*;
import java.awt.event.*;
import java.applet.*;
import java.awt.geom.*;
import java.math.*;
import java.util.Arrays;


/**This file contains the proof that the renormalization map
   brings together any points x,y in [0,2] such that 
   x-y = m + n phi  and max(|m|,|n|)<100.  The main test
   shows the following implication:

   if x-y = m+ n phi as above, then x-->x* and y-->y*, where

   x*-y* or y*-x* is one of

   0              (case 1)
   2 - 2 phi      (case 2)
   4 - 2 phi      (case 3)

   In case 2, one more renormalization brings the points together.
   In Case 3, another renormalization either reduces to case 1 or 2,
   or else x lies in I2 or I4, and renormalization of both points
   gives another instance of case 3.   We check these cases separately.**/


    


public class ProofArithmetic implements Runnable {
    int halt;
    Manager M;


public ProofArithmetic(Manager MM) {
    this.M=MM;
}


    public void failMessage() {
	throw new ProofException("Proof Arithmetic");
    }


    public void run() {
	mainTest();
	auxTest();
    }




   /**Here is the main test.  This test shows that if
    x-y = m + n phi  and max(|m|,|n|)<100 then
    x-->x* and y-->y*, where x*-y* or y*-x* is one of
    0              (case 1)
    2 - 2 phi      (case 2)
    4 - 2 phi      (case 3)

    The test works as follows.  We let the renormalization
    map act on the square [0,2]^2, by acting on each
    coordinate separately.  Our choice of x and y means
    that (x,y) lies on one of finitely many lines segments
    of slope1.  Let P be an initial segment.  We perform
    2 steps repeatedly:

    1.  As subdivide P into intervals on which R or R^2
        is entirely defined.  We use R^2 on the intervals
        where R is an isometry.  So, the map we apply always
        dilates by phi^3.

    2.  We let R act on each interval.  This gives us a new
        list of intervals which we add to our list of
        intervals to be processed.

    We "pass" any interval that lies on a diagonal line
    corresponding to one of the 3 values above.  The
    routine stops when our list is empty.  **/





    public void mainTest() {
	GoldenReal[] X=specialList();
	for(int i=0;i<X.length;++i)  {
	    X[i].printNoLine();
            verify(X[i]);
	}
    }

    public void verify(GoldenReal X) {
	GoldenPolyWedge[] LIST=new GoldenPolyWedge[100];
	int total=1;
	LIST[0]=diagonal(X);
	while(total>0) {
	    GoldenPolyWedge P=LIST[total-1];

	    GoldenReal r1=P.z[0].x;
	    GoldenReal r2=P.z[0].y;
	    GoldenReal r3=GoldenReal.plus(r1,new GoldenReal(-2,2));
	    GoldenReal r4=GoldenReal.plus(r1,new GoldenReal(4,-2));
	    boolean test1=GoldenReal.equals(r1,r2);
	    boolean test2=GoldenReal.equals(r3,r2);
	    boolean test3=GoldenReal.equals(r4,r2);
	    if((test1==true)||(test2==true)||(test3==true)) --total;
	    else {
		--total;
		GoldenPolyWedge[] Q=subdivide(P);
		for(int i=0;i<Q.length;++i) {
		    LIST[total]=act(Q[i]);
		    ++total;
		}
	    }
	}
	System.out.println("  pass");
    }



    /**THE ACTION ON THE INTERVALS**/

    /**This is the routine where we act on our
       intervals. They are stored as "polygons"
       with 2 vertices.**/

    public GoldenPolyWedge act(GoldenPolyWedge P) {
	testSmall(P);   //makes sure R or R^2 is defined
	testDiagonal(P); //makes sure P is one of the diagonal segments

	GoldenReal X=GoldenReal.interpolate(P.z[0].x,P.z[1].x);
	GoldenReal Y=GoldenReal.interpolate(P.z[0].y,P.z[1].y);
	int kX=interval(X);
	int kY=interval(Y);

	GoldenPolyWedge Q=new GoldenPolyWedge();
	Q.count=2;
	Q.z[0]=new GoldenComplex();
	Q.z[1]=new GoldenComplex();
	Q.z[0].x=map(kX,P.z[0].x);
	Q.z[0].y=map(kY,P.z[0].y);
	Q.z[1].x=map(kX,P.z[1].x);
	Q.z[1].y=map(kY,P.z[1].y);
	Q=swap(Q);
	testDiagonal(Q);  //not needed, but just to be sure.
	return(Q);
    }


    /**swaps the coords to that the first one is smaller.**/

    public GoldenPolyWedge swap(GoldenPolyWedge P) {
	GoldenPolyWedge Q=new GoldenPolyWedge();
	Q.count=2;
	Q.z[0]=new GoldenComplex(P.z[0]);
	Q.z[1]=new GoldenComplex(P.z[1]);
	if(GoldenReal.isLess(Q.z[0].x,Q.z[0].y)==false) Q.z[0]=swap2(Q.z[0]);
	if(GoldenReal.isLess(Q.z[1].x,Q.z[1].y)==false) Q.z[1]=swap2(Q.z[1]);
	if(GoldenReal.isLess(Q.z[0].x,Q.z[1].x)==false) Q=swap1(Q);
	return(Q);
    }

    public GoldenPolyWedge swap1(GoldenPolyWedge P) {
	GoldenPolyWedge Q=new GoldenPolyWedge();
	Q.count=2;
	Q.z[0]=new GoldenComplex(P.z[1]);
	Q.z[1]=new GoldenComplex(P.z[0]);
	return(Q);
    }

    public GoldenComplex swap2(GoldenComplex z) {
	return(new GoldenComplex(z.y,z.x));
    }
  



    /**SUBDIVISION ALGORITHM**/

    /**This divides each segment into a union of segments
       on which the renormalization map is coherently
       defined.  This means that the x coords of all points
       lie in the same partition interval and the y-coords
       of all points lie in the same interval.  The x-invarval
       and the y-interval might be distinct.**/

    public GoldenPolyWedge[] subdivide(GoldenPolyWedge P) {
	testDiagonal(P);
	GoldenComplex[] Z=divisionPoints(P);
	if(Z==null) {
	    GoldenPolyWedge[] Q=new GoldenPolyWedge[1];
	    Q[0]=P;
	    return(Q);
	}
	GoldenPolyWedge[] Q=new GoldenPolyWedge[Z.length-1];
	for(int i=0;i<Z.length-1;++i) {
	    Q[i]=new GoldenPolyWedge();
	    Q[i].count=2;
	    Q[i].z[0]=new GoldenComplex(Z[i]);
	    Q[i].z[1]=new GoldenComplex(Z[i+1]);
	    testDiagonal(Q[i]);
	}
	return(Q);
    }


    /**This produces all the partition points that lie on the
       segment defined by P.  First we produce an unordered
       list and then we sort.  We use floating point arithmetic
       to sort, so we then check that the sorted list matches
       the original list.**/

    public GoldenComplex[] divisionPoints(GoldenPolyWedge P) {	
        GoldenReal s=GoldenReal.minus(P.z[0].y,P.z[0].x);
	GoldenComplex[] Z=divisionPointsRaw(P);
	if(Z==null) return(null);

	double[] d=new double[Z.length];
	for(int i=0;i<Z.length;++i) {
            d[i]=Z[i].x.toDouble();
	}

	Arrays.sort(d);
	GoldenReal[] g=new GoldenReal[Z.length];
	for(int i=0;i<Z.length;++i) g[i]=new GoldenReal(d[i],20,.0000001);

	if(s.isPositiveOrZero()==false) failMessage();


	GoldenComplex[] W=new GoldenComplex[Z.length];
	for(int i=0;i<Z.length;++i) {
            W[i]=new GoldenComplex(g[i],GoldenReal.plus(g[i],s));
	}
	if(Lists.match(Z,W,Z.length)==false) failMessage();
	return(W);
    }


    public GoldenComplex[] divisionPointsRaw(GoldenPolyWedge P) {
	GoldenReal s=GoldenReal.minus(P.z[0].y,P.z[0].x);
	GoldenComplex[] LIST=new GoldenComplex[15];
	LIST[0]=new GoldenComplex(P.z[0]);
	int total=1;
	for(int i=0;i<6;++i) {
	    GoldenReal r1=cut(i);
	    GoldenReal r2=GoldenReal.plus(r1,s);
	    GoldenReal r0=GoldenReal.minus(r1,s);

	    boolean test=true;
	    if(GoldenReal.isLess(r1,P.z[0].x)==true) test=false;
	    if(GoldenReal.isLess(P.z[1].x,r1)==true) test=false;
	    if(GoldenReal.isLess(P.z[0].x,r1)==false) test=false;
	    if(GoldenReal.isLess(r1,P.z[1].x)==false) test=false;
	    if(test==true) {
		LIST[total]=new GoldenComplex(r1,r2);
		++total;
		if(r2.toDouble()>2.00001) failMessage();
	    }

            test=true;
	    if(GoldenReal.isLess(r1,P.z[0].y)==true) test=false;
	    if(GoldenReal.isLess(P.z[1].y,r1)==true) test=false;
	    if(GoldenReal.isLess(P.z[0].y,r1)==false) test=false;
	    if(GoldenReal.isLess(r1,P.z[1].y)==false) test=false;
	    if(test==true) {
		LIST[total]=new GoldenComplex(r0,r1);
		++total;
		if(r0.toDouble()<-.00001) failMessage();
	    }
	}
	LIST[total]=new GoldenComplex(P.z[1]);
	++total;
	return(Lists.clean(LIST,total));
    }



    /**CHECKS**/

    /*This makes sure that the segment has slope 1. 
      and that everything is in correct order.**/

    public void testDiagonal(GoldenPolyWedge P) {
	if(GoldenReal.isLess(P.z[0].y,P.z[0].x)==true) failMessage();
	if(GoldenReal.isLess(P.z[1].y,P.z[1].x)==true) failMessage();
	if(GoldenReal.isLess(P.z[1].x,P.z[0].x)==true) failMessage();
	GoldenReal y=GoldenReal.minus(P.z[1].y,P.z[0].y);
	GoldenReal x=GoldenReal.minus(P.z[1].x,P.z[0].x);
	if(GoldenReal.equals(x,y)==false) failMessage();
    }


    /**This tests if the interval [r1,r2] is contained on one of
       the 6 partition intervals.**/

    public boolean testSmall(GoldenReal r1,GoldenReal r2) {
	if(GoldenReal.equals(r1,r2)==true) return(true);

	for(int i=0;i<5;++i) {
	    GoldenReal s1=cut(i);  
            GoldenReal s2=cut(i+1);
	    boolean test1=GoldenReal.isLess(r1,s1);
	    boolean test2=GoldenReal.isLess(r2,s1);
	    boolean test3=GoldenReal.isLess(s2,r1);
	    boolean test4=GoldenReal.isLess(s2,r2);
	    if((test1==false)&&(test2==false)&&(test3==false)&&(test4==false)) return(true);
	}
	return(false);
    }

    public void testSmall(GoldenPolyWedge P) {
	boolean test1=testSmall(P.z[0].x,P.z[1].x);
	boolean test2=testSmall(P.z[0].y,P.z[1].y);
	if(test1==false) failMessage();
	if(test2==false) failMessage();
    }







    /**RENORMALIZATION MAP**/

    public int interval(GoldenReal r) {
	for(int i=0;i<6;++i) {
	    GoldenReal s1=cut(i);  
            GoldenReal s2=cut(i+1);
	    boolean test1=GoldenReal.isLess(r,s1);
	    boolean test2=GoldenReal.isLess(s2,r);
	    if((test1==false)&&(test2==false)) return(i);
	}
	return(-1);
    }

    public GoldenReal map(int k,GoldenReal r) {
	GoldenReal t=translationPart(k);
	GoldenReal s=GoldenReal.times(r,new GoldenReal(1,2));
	s=GoldenReal.plus(s,t);
	return(s);
    }


    public GoldenReal translationPart(int k) {
	int[][] A={{0,0},{2,-2},{0,-2},{-2,-2},{0,-4}};
	GoldenReal t=new GoldenReal(A[k][0],A[k][1]);
	return(t);
    }


    public static GoldenReal cut(int n) {
	int[][] A={{0,0},{2,-1},{4,-2},{-2,2},{0,1},{2,0}};
	if(n<0) return(new GoldenReal(0,0));
	if(n>5) return(new GoldenReal(2,0));
	return(new GoldenReal(A[n][0],A[n][1]));
    }



    /**CREATION OF INTERVALS**:
       This create the diagonal line x+y=r intersected with [0,2]^2.**/

    public GoldenPolyWedge diagonal(GoldenReal r) {
	GoldenReal s=new GoldenReal(2-r.a[0],-r.a[1]);
	GoldenPolyWedge P=new GoldenPolyWedge();
	P.count=2;
	P.z[0]=new GoldenComplex(new GoldenReal(0,0),r);
	P.z[1]=new GoldenComplex(s,new GoldenReal(2,0));
	return(P);
    }


    public GoldenReal[] specialList() {
	GoldenReal TWO=new GoldenReal(2,0);
	GoldenReal[] LIST1=new GoldenReal[200];
	int total=0;
	for(int i=-100;i<=100;i=i+2) {
	    for(int j=-100;j<=100;j=j+2) {
		GoldenReal r=new GoldenReal(i,j);
		boolean test1=r.isPositive();
		boolean test2=GoldenReal.isLess(r,TWO);
		if((test1==true)&&(test2==true)) {
		    LIST1[total]=r;
		    ++total;
		}
	    }
	}
	return(Lists.clean(LIST1,total));
    }


    /**AUXILLIARY TESTS**/


/**These tests deal with case 3 of the main test. Each test shows that
   case 3 "works" when x lies in certain intervals. We want to see that
   
   -- case 3, and x AND y in I2 leads back to case 3
   -- case 3, and x OR y in I2 union I3 leads to cases 1,2.
**/

    public void auxTest() {
	auxTest1();
	auxTest2A();
	auxTest2B();
	auxTest3A();
	auxTest3B();
    }


    /**deals with interval 1**/

    public void auxTest1() {
	System.out.println("aux 1");
	GoldenReal r1=new GoldenReal(0,0);
	GoldenReal r2=new GoldenReal(2,-1);
	GoldenReal r3=new GoldenReal(4,-2);
	GoldenReal r4=new GoldenReal(6,-3);
	GoldenPolyWedge P=new GoldenPolyWedge();
	P.count=2;
	P.z[0]=new GoldenComplex(r1,r3);
	P.z[1]=new GoldenComplex(r2,r4);
	aux(P);
    }


    /**deals with interval 2**/

    public void auxTest2A() {
  	System.out.println("aux 2A");
	GoldenReal r1=new GoldenReal(2,-1);
	GoldenReal r2=new GoldenReal(-6,4);
	GoldenReal r3=new GoldenReal(6,-3);
	GoldenReal r4=new GoldenReal(-2,2);
	GoldenPolyWedge P=new GoldenPolyWedge();
	P.count=2;
	P.z[0]=new GoldenComplex(r1,r3);
	P.z[1]=new GoldenComplex(r2,r4);
	aux(P);
    }

    /**Here x and y both belong to I2.  This is
       the only time we get back to Case 3.**/

    public void auxTest2B() {
 	System.out.println("aux 2B");
	GoldenReal r1=new GoldenReal(-6,4);
	GoldenReal r2=new GoldenReal(4,-2);
	GoldenReal r3=new GoldenReal(-2,2);
	GoldenReal r4=new GoldenReal(8,-4);
	GoldenPolyWedge P=new GoldenPolyWedge();
	P.count=2;
	P.z[0]=new GoldenComplex(r1,r3);
	P.z[1]=new GoldenComplex(r2,r4);
	aux(P);
    }



    /**deals with interval 3**/

    public void auxTest3A() {
  	System.out.println("aux 3A");
	GoldenReal r1=new GoldenReal(4,-2);
	GoldenReal r2=new GoldenReal(-4,3);
	GoldenReal r3=new GoldenReal(8,-4);
	GoldenReal r4=new GoldenReal(0,1);
	GoldenPolyWedge P=new GoldenPolyWedge();
	P.count=2;
	P.z[0]=new GoldenComplex(r1,r3);
	P.z[1]=new GoldenComplex(r2,r4);
	aux(P);
    }

    public void auxTest3B() {
	System.out.println("aux 3B");
	GoldenReal r1=new GoldenReal(-4,3);
	GoldenReal r2=new GoldenReal(1,0);
	GoldenReal r3=new GoldenReal(0,1);
	GoldenReal r4=new GoldenReal(5,-2);
	GoldenPolyWedge P=new GoldenPolyWedge();
	P.z[0]=new GoldenComplex(r1,r3);
	P.z[1]=new GoldenComplex(r2,r4);
	P.count=2;
	aux(P);
    }

    public void aux(GoldenPolyWedge P) {
	GoldenPolyWedge Q=act(P);
	GoldenReal r=GoldenReal.minus(Q.z[0].y,Q.z[0].x);
	r.print();
    }






}