import java.applet.Applet; import java.awt.*; import java.awt.event.*; import java.applet.*; import java.awt.geom.*; import java.math.*; public class Proof implements Runnable { Manager M; BoxConfiguration[] LIST=new BoxConfiguration[1000]; BoxConfiguration CONFINE; int halt,COUNT,VOLUME,SEC1,SEC2,INTERVAL; double ENERGY,TETRA; Interval IENERGY,ITETRA,CONFINE_RADIUS; double TOTAL,TIME; int[] MISMATCH={0,0,0,0}; Complex[] TBP=new Complex[4]; IntervalComplex[] ITBP=new IntervalComplex[4]; int[] LOG=new int[10000]; public Proof() { COUNT=1; LIST[0]=BoxConfiguration.initialBox(); } public Proof(Manager MM) { this.M=MM; halt=0; setInitialConditions(); } public void setInitialConditions() { COUNT=1; LIST[0]=BoxConfiguration.initialBox(); VOLUME=BoxConfiguration.volumeLog(LIST[0]); CONFINE=M.P.getBC(1); setTBP(); } public void setTBP() { TBP[0]=new Complex(1,0); TBP[1]=new Complex(-.5,-Math.sqrt(3.0)/2.0); TBP[2]=new Complex(0,0); TBP[3]=new Complex(-.5,Math.sqrt(3.0)/2.0); for(int i=0;i<4;++i) { ITBP[i]=IntervalComplex.fat(TBP[i]); } } public void run() { initialize(); int k=M.C.CONFINE.val; //radius of confinement double E=M.C.ENERGY.getParameter(); //power law exponent while((halt==1)&&(COUNT>0)) mainStep(E,k); finalize(); } public void initialize() throws ProofException { for(int i=0;i<200;++i) LOG[i]=0; halt=1; TOTAL=0; TIME=System.currentTimeMillis(); SEC1=0; double E=M.C.ENERGY.getParameter(); INTERVAL=M.C.PC.INTERVAL.on; //interval arithmetic ENERGY=Energy.minEnergy(E); TETRA=Energy.tetrahedralComplement(E); if(INTERVAL==1) IENERGY=IntervalEnergy.minEnergy(E); if(INTERVAL==1) ITETRA=IntervalEnergy.tetrahedralComplement(E); sendMessage(); if(INTERVAL==1) { if((E!=1.0)&&(E!=2.0)) { throw new ProofException("interval arithmetic only runs with exponent 1 or 2"); } } } public void finalize() { sendMessage(); halt=0; } /**The main step in the algorithm. k is the confine radius**/ public void mainStep(double E,int k) { int[] test={0,0}; BoxConfiguration X=new BoxConfiguration(LIST[COUNT-1]); int mode=M.C.PC.SI[0].val; if(mode==0) test=determineAction(E,k,X); //the basic proof if(mode==1) { test=XtraProof.determineAction(M.C.PC,E,k,X,CONFINE,ENERGY,TETRA,TBP); } //advanced mode if(test[0]==0) subdivide(X,test[1]); if(test[0]==1) eliminate(X); displayStats(); } /**The main test. E is the exponent for the power law. k is the confine radius. The goal is to confine the particles to be inside boxes of sidelength 2^{-k} about the TBP. X is the current configuration. **/ public int[] determineAction(double E,int k,BoxConfiguration X) { if(INTERVAL==0) return(determineActionFloatingPoint(E,k,X)); else return(determineActionIntervalArithmetic(E,k,X)); } public int[] determineActionFloatingPoint(double E,int k,BoxConfiguration X) { int[] pass={1,0}; if(BoxConfiguration.near(k,TBP,X)==1) return(pass); if(RedundancyEliminator.eliminate(E,X)==1) return(pass); if(TetrahedralEliminator.eliminate(TETRA,E,X)==1) return(pass); int[] t=EnergyEstimator.eliminate(ENERGY,E,X); if(t[0]==1) return(pass); return(t); } public int[] determineActionIntervalArithmetic(double E,int k,BoxConfiguration X) { int[] pass={1,0}; if(BoxConfiguration.near(k,TBP,X)==1) { IntervalBoxConfiguration XX=IntervalBoxConfiguration.create(X); if(IntervalBoxConfiguration.near(k,ITBP,XX)==1) return(pass); ++MISMATCH[0]; System.out.println("mismatch 0: "+MISMATCH[0]); } if(RedundancyEliminator.eliminate(E,X)==1) { IntervalBoxConfiguration XX=IntervalBoxConfiguration.create(X); if(IntervalRedundancyEliminator.eliminate(E,XX)==1) return(pass); ++MISMATCH[1]; System.out.println("mismatch 1: " +MISMATCH[1]); } if(TetrahedralEliminator.eliminate(TETRA,E,X)==1) { IntervalBoxConfiguration XX=IntervalBoxConfiguration.create(X); if(IntervalTetrahedralEliminator.eliminate(ITETRA,E,XX)==1) return(pass); ++MISMATCH[2]; System.out.println("mismatch 2: " +MISMATCH[2]); } int[] t=EnergyEstimator.eliminate(ENERGY,E,X); if(t[0]==1) { IntervalBoxConfiguration XX=IntervalBoxConfiguration.create(X); int u=IntervalEnergyEstimator.eliminate(IENERGY,E,XX); if(u==1) return(pass); ++MISMATCH[3]; System.out.println("mismatch 3: " +MISMATCH[3]); } t[0]=0; return(t); } /**The two options for the current configuration */ /** elimination**/ public void eliminate(BoxConfiguration X) { ++LOG[14+BoxConfiguration.volumeLog(X)]; M.P.Z[0]=BoxConfiguration.toComplex(X); for(int i=0;i<4;++i) M.C.CC1.size[0][i]=X.B[i].k; if(M.C.SHOW.L[5].on==1) M.P.repaint(); --COUNT; } /**Subdivision: The integer q tells which subdivision to perform.**/ public void subdivide(BoxConfiguration X,int q) { --COUNT; if(q==0) { for(int n=0;n<2;++n) { LIST[COUNT]=X.subdivide1(n); ++COUNT; } } if(q!=0) { for(int n=0;n<4;++n) { LIST[COUNT]=X.subdivide0(q,n); ++COUNT; } } } /**These routines aren't part of the proof, but they are used to mark the progress of the program.**/ /**This routine computes the elapsed time and updates the display after each second passes.**/ public void displayStats() { SEC2=SEC1; double[] time=new double[10]; time[0]=TIME; time[1]=System.currentTimeMillis(); time[2]=(time[1]-time[0])/1000; SEC1=(int)(time[2]); if(SEC1!=SEC2) sendMessage(); } /**We store the volume of the space computed as a list of the logs of the volumes of the boxes that have been eliminated. This makes for an accurate computation and avoids roundoff error.**/ public void computeVolume() { double total=0; for(int i=0;i<200;++i) { total=total+LOG[i]*Math.pow(.5,i); } total=total*Math.pow(2,VOLUME+14); TOTAL=total; } public void sendMessage() { computeVolume(); M.C.PC.time=SEC1; //elapsed time M.C.PC.progress=TOTAL; //volume eliminated M.C.repaint(); } }