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


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

    public void proofInfo() {

	String S="proof controls";

	S=S+"\n\nThese controls let you manage the rigorous proofs.  There are 8 basic divisions in these controls:";

	S=S+"\n\n1 pinwheel: This does the proofs for the Pinwheel Lemma.";

	S=S+"\n\n2 compactify: This does the proofs for the Compactification Theorem.";

	S=S+"\n\n3 fundamental: This does the proofs for the Fundamental Orbit Theorem";

	S=S+"\n\n4 fixed point: This does the proofs for the Fixed Point Theorem";

	S=S+"\n\n5 reduction 1: This does the proofs for the Near reduction Theorem.";

	S=S+"\n\n6 reduction 2: This does the proofs for the Far reduction Theorem.  The test samples all the A-chains and B-chains and makes the combinatorial test. There isn't more we will say about it, though there is separate documentation for the chain selector that pops up when you select this option.";

	S=S+"\n\n7 renormalize: This does the proofs for the Renormalization Theorem.  This really the main test.";

	S=S+"\n\n8 arithmetic: This does the proof for the Descent Lemma II.  The test is exactly as described in the paper, and we do not say more about it here. The code is contained in the file ProofArithmetic.java.";

	S=S+"\n\nEach unit (except 6 and 8) is broken up into smaller units, so that one can perform the tests in smaller chunks.  The control panels managing these chunks have more documentation about the tests.";

	S=S+"\n\nAll the calculations are done with exact integer arithmetic, using longs.  The integers involved are much, much smaller than what would cause an overflow error. Nonetheless, we have set things up so that you can check that no overflow error happens.  In order to use this feature, you have to go into the GoldenReal class and uncomment the 6 lines that call the tooBig checker.  The reason we turn this off for the normal running of the program is that it slows things down by a huge amount.   Also, we only have to do the rigorous proofs once.";

	M.D.setExplain(S);
	M.D.repaint();
    }


    public void pinwheelInfo() {

	String S="pinwheel proof controls";

	S=S+"\n\nThese controls let you manage the rigorous proofs for the Pinwheel Lemma.  The candidate list of first return tiles are listed in raw form in DataPinwheelRaw.java and accessed through commands in DataPinwheel.java.  There proof is broken into 4 tests";

	S=S+"\n\n1 cover: This checks that the listed return tiles cover the region [-20,20] x [-2,2]. After the rest runs, the tiles are plotted, as a visual sanity check. The code for this check is in the file ProofPinwheel1.java.";

	S=S+"\n\n2 definedness 1: This checks that the first return map to the strip Sigma = R x [-2,2] is well defined on the interiors of all the listed return tiles, and that the square of the first return map is undefined on the boundary edges of the return tiles.  This shows that we really have got the correct return tiles.  This corresponds to the statement in the paper that the tiles we have are Psi-perfect. There is one caveat: the horizontal segments contained in the line y=0 are just artifacts of the way we produce the tiles.  They cut through the middle of the tiles, and are not boundary edges. Our calculations ignore these.  The code for these tests is again in ProofPinwheel1.java";  

	S=S+"\n\n3 definedness 2: This checks that the pinwheel map Pi is everywhere defined on the interiors of the list of return tiles and that no boundary point has a well defined Pi orbit. For the undefinedness test, we check that an edge either maps into the boundary of a pinwheel strip, or that it maps to a non-horizontal boundary segment of Sigma_+ union Sigma_-. As explained in the paper, this suffices. This establishes the statement in the paper that these tiles are Pi-perfect.  This code for this is contained in the file ProofPinwheel2.java";

	S=S+"\n\n4 equality: This checks that Pi=Psi on each pinwheel tile. We compute the symbolic dynamics associated to each map and check that it leads to the same translation. The code for this is contained in the file ProofPinwheel3.java.";

	M.D.setExplain(S);
	M.D.repaint();
    }


    public void compactInfo() {

	String S="compactification proof controls";

	S=S+"\n\nThese controls let you manage the rigorous proofs for the Compactification Theorem.";

	S=S+"\n\n The outer billiards tiles are listed in raw form in DataPinwheelRaw.java and accessed through commands in DataPinwheel.java.  The code for the test is contained in the files ProofCompact1.java and ProofCompact2.java";


	S=S+"\n\n The polyhedron exchange tiles are listed in raw form in DataPartitionRaw.java and accessed through commands in DataPartition.java.";

	S=S+"\n\nThe proofs are broken down into two parts";

	S=S+"\n\n1 cover: This checks that the 64 polyhedra listed really do cover the 3-torus. There are 4 sub-tests we perform:";

	S=S+"\n\nplatinum test: We check that each polyhedron, when sliced by an arbitrary horizontal plane of golden height, is a golden polygon.  The criterion is just an arithmetic statement about the coordinates about the vertices, as explained in the paper.";

	S=S+"\n\nconvex test: We check that each polyhedron is strictly convex.";

	S=S+"\n\ndisjoint test: We check that the polyhedra have pairwise disjoint interiors.";

	S=S+"\n\ncover test: We now check the covering property using the slicing method discussed in the paper. This amounts to checkings things at 10 horizontal slices.  The heights we use are interlaced with the 11 heights of horizontal planes that contain polyhedron vertices.";


	S=S+"\n\ndefinedness: we check that a certain 4 dimensional lift of the pinwheel map is well defined on each of the 64 polyhedra.  This is the only place where we use the 4-dimensional data structures, such as GoldenPolytope.  This test and the covering test combine with the theoretical work in the paper to establish the compactification theorem.";


	M.D.setExplain(S);
	M.D.repaint();
    }



    public void fundamentalInfo() {

	String S="fundamental orbit proof controls";

	S=S+"\n\nThese controls let you manage the rigorous proofs for the Fundamental Orbit Theorem.  The code for the test is contained in the file ProofFundamental.java  The tests involve 6 small triangles, contained in the fundamental triangle and its mirror image.  There test is broken up (somewhat arbitrarily) into 7 pieces.";


	S=S+"\n\n1 cover: This checks that the polygons we have listed really do cover the 6 little triangles.";

	S=S+"\n\nThe remaining 6 tests check that each polygon P in each cover satisfies the basic equation that needs to hold for the Fundamental Orbit Theorem. That is:";

	S=S+"\n\nP is contained in an A-atom.  In fact P equals this A-atom, but we do not explicitly check this, or need to check it.";

	S=S+"\n\nThe renormalization Q of P is such that psi(Q) and P are related by one of the dilations taking the little triangle containing P to either the fundamental triangle or its mirror.";

	S=S+"\n\nThere is one test per little triangle.  As the test runs, the polygons are plotted in the outer billiards window. This serves as a sanity check that the program is functioning correctly.";

	M.D.setExplain(S);
	M.D.repaint();
    }



    public void fixedInfo() {

	String S="fixed point proof controls";

	S=S+"\n\nThese controls let you manage the rigorous proofs for the Fixed Point Theorem. The code for the tests is in the file ProofFixedPoint.java. The tests work exactly the same as for the Fundamental Orbit Theorem, except this time there is just one region, Q1, rather than the 6 little triangles.  So, we have the covering test and the main test.  The same sanity check runs as for the Fundamental Orbit Theorem.";

	M.D.setExplain(S);
	M.D.repaint();
    }



    public void reduce1Info() {

	String S="Near Reduction Proof controls";

	S=S+"\n\nThese controls let you manage the rigorous proofs for the Near Reduction Theorem. The code for the tests is contained in the file ProofReduce1.java.  The polygons used during the proofs are stored in raw form in the file DataReductionRaw.java and accessed through commands in the file DataReduction.java.  The tests here are broken into 7 units:";

	S=S+"\n\ncover. This checks that the relevant partitions cover the relevant polygons.  This is similar to what is done for the Fundamental Orbit Theorem and the Fixed Point Theorem.";

	S=S+"\n\nvalidity1: This checks that each of the polygons contained in the 23 PSRT's (positive symmetric return-1 tiles) is contained in an A-atom. This is a long test, involving about 900 polygons divided into 23 groups.";

	S=S+"\n\nvalidity2: This checks that we have correctly computed the renormalizations of the 12 super taut polygons.";

	S=S+"\n\nvalidity3: This checks that the second renormalizations of the 12 super taut polygons are containe din A-atoms.";

	S=S+"\n\ntaut: This verifies that our list of taut tiles, a subset of about 100 tiles from amongst the original 900, is correct.  Basically, we re-generate the list and see that it matches what we have already stored.";

	S=S+"\n\nsuper taut: This verifies that our list of 12 super taut tiles is correct. Again, it re-generates the list and checks that it matches what we have already stored.";

	S=S+"\n\nsuper taut renorm: This verifies that the second renormalizations of 10 of the 12 super taut tiles lie closer to the y-axis (by at least 2phi^{-3}) than the original super-tau tiles.  The paper handles the two exceptional super taut tiles by hand.";

	M.D.setExplain(S);
	M.D.repaint();
    }


    public void renormInfo() {

	String S="Renormalization Test controls";

	S=S+"\n\nThese controls let you manage the rigorous proofs for the Renormalization Theorem. This is the main test.";

	S=S+"\n\n  The code for the tests is contained in the files ProofRenorm1.java ... ProofRenorm5.java.  The code in the file ProofRenorm1.java corresponds to part 1 below, and so on.";

	S=S+"\n\n  The A and B renormalization sets can be found, in raw form, in the file DataRenormRaw.java.  They are accessed using commands in the file DataRenorm.java.";

	S=S+"\n\n  The atoms can be found, in raw form, in the file DataRenormReturnRaw.java.  They are accessed using commands in the file DataRenormReturn.java.";

	S=S+"\n\n Here are the 5 parts of the overall test:";

	S=S+"\n\nvalidity. This checks that the A-atoms and the B-atoms are indeed atoms, and they the renormalization map R gives a correspondence between them in the way that is advertised in Statement 1 of the Renormalization Theorem.";

    S=S+"\n\ncover 1: This checks that the listed A-atoms partition the A renormalization set, and likewise for B.";

S=S+"\n\n cover 2: This checks that the 10 special polyhedra in the polyhedron exchange map are partitioned into a union of B-atoms and periodic tiles.  Using the auxilliary controls, you can test the indices (i,j) separately, where i indexes one of the 10 polyhedra, and j indexes one of the 3 bottom layers of that polyhedron. As discussed in the paper, this suffices to prove what we need.";

S=S+"\n\n cover 3: This checks that the B renormalization set is partitioned into a union of A-atoms and periodic tiles.  Using the auxilliary controls, you can test the indices (i,j)$ separately, where i indexes one of the bottom 9 layers and j indexes one of the 4 branches in that layer.  As discussed in the paper, this suffices for our purposes.  This test is by far the longest one.  It takes several hours without the overflow checker. It takes about 24 hours with the overflow checker.  These time are with respect to my 2010 macbook pro laptop.";

S=S+"\n\nB maximality:  This tests that the B-atoms really are maximal, in the sense that every face of a listed B-atom either maps into a crack of the polyhedron exchange map, or else into the boundary of the B renorm set.  This shows that the first return map to the B renorm set cannot be defined on any boundary point of one of the listed atoms.";


	M.D.setExplain(S);
	M.D.repaint();
    }



    public void zoneInfo() {

	String S="Zone selector";

	S=S+"\n\nThese controls let you specify which of the 10 special polyhedra you want to involve in the cover 2 test. You can select as many or as few of them as you like.  Of course, they all must be tested for theproof to be valid.";

	M.D.setExplain(S);
	M.D.repaint();
    }


    public void layerInfo() {

	String S="layer selector";

	S=S+"\n\nThese controls let you specify which of the 3 B-layers you want to involve in the cover 2 test. You can select as many or as few of them as you like.  Of course, they all must be tested for theproof to be valid.";

	M.D.setExplain(S);
	M.D.repaint();
    }






}