@i verify.format
@*Overview.
The purpose of this program is to be used in the proof of:

Theorem.
Let $N$ be a closed orientable hyperbolic
3-manifold.  Then if $f:M\to N$ is a homotopy equivalence where $M$ 
is an irreducible manifold, then $f$ is  homotopic to a homeomorphism.

The details of the proof and how it uses the result of this program
are beyond the scope of this document.
It is not so clear what exactly the scope should be,
but I have chosen to make it as narrow as possible,
with occasional references to higher-level concepts.

I have made an effort to make this program comprehensible to mathematicians
without an extensive background in programming.
It is written in \CEE/++, but mostly it is a \CEE/ program -- the only
departures from \CEE/ are in defining expressions like |x+y| when
|x| and |y| are composite types (e.g., complex numbers), and
for constructing composite types (e.g., |XComplex(a,b)|) from
their component parts, and declaring variables as they are needed
(instead of at the beginning of the function).
My hope is that anyone who has written a short \CEE/ program will
be able to understand this program.

This draft includes the program, and statements of the lemmas
needed for a proof of its correctness.

If $g,h \in \PSLC$, we will define the
translation length $L(g) \in \Complex$ of $g$
and the ortholength $L_h(g) \in \Complex$ of $g$ with respect to $h$.

A pair $(f,w) \in \PSLC$ is minimal if,
for all $g \in <f,w>, g \ne I$,
(i) $\abs{L(f)} \le \abs{L(g)}$ and
(ii) $\abs{L_f(w)} \le \abs{L_f(g)}$.

We will define maps
$s : \Complex \ra \PSLC$ and
$c : \Complex^2 \ra \PSLC$,
and a domain $D \subset \Complex^3$
(chosen so that $(s,c) : \Complex^3 \ra \PSLC\cross\PSLC$ covers the space
of groups of interest, modulo conjugation).

We will also define a ``recursive partition''
$Z : \{0,1\}^* \ra 2^{\Complex^3}$ of $D$ such that
$Z(s) = Z(s 0) \union Z(s 1)$ for all $s \in \{0,1\}^*$
and $Z(\lambda) \supset D$.

If $R \subset \Complex^3$, and if $(s(x_0), c(x_1,x_2))$ is not minimal
for any $x \in R \intersect D$, we say that $R$ is MNG-free.

\lemma
If this program finishes, and prints
``verified $p$ - $\{ m_0\ m_1\ \ldots\ m_k \}$.'',
then $Z(p) - \Union_i Z(m_i)$ is MNG-free.
\endlemma

The input to the program is a sequence of integers,
which encode how the proof is to be carried out.
This input can affect how long the program will run,
and determines whether or not it will finish,
but does not affect the correctness of its proof.
All of these inputs were produced by programs,
some of which are a good deal more complicated than this one,
but fortunately they are also beyond the present scope.
It suffices to treat the inputs as oracular advice.

@ The program will split the proof into many pieces.
For each piece $Z(p_i)$, it will either show
that $Z(p_i) \intersect D$ is empty or show that
$(s(x_0),c(x_1,x_2))$ is not minimal for any $x \in Z(p_i)$.
In the second case, this is an exhibition that (i) or (ii) does not hold:
a word $a$ in the free group generated by the symbols $f$ and $w$
such that 
$g \ne I$, $g \ne -I$,
and either
(i) $\abs{L(g)} < \abs{L(f)}$
or
(ii) $\abs{L_f(g)} < \abs{L_f(w)}$
whenever
$f = s(x_0), w = c(x_1, x_2)$,
$g$ is the corresponding product,
and $x \in Z(p_i)$.

If we treat $L(f)$, $L(g)$, $L_f(w)$, and $L_f(g)$
as functions from $Z(p_i)$ to $\Complex$,
the problem can be thought of in terms of bounding the range
of $\abs{L(g)/L(f)}$ and $\abs{L_f(g)/L_f(w)}$.

To get these bounds, we work with local complex-affine approximations:
given $(f,f_0,f_1,f_2, \epsilon)$,
the class of all functions $g : H \ra \Complex$ 
such that $\abs{g(x) - (f + f_0 x_0 + f_1 x_1 + f_2 x_2)} < \epsilon$
for all $x \in H$,
where $H$ is $D^3$:
$H = \{z : \abs{z_i} <= 1, \hbox{ for } i=0,1,2\}$.

Each of the functions we use is constructed from simple functions
using only addition, subtraction, multiplication, division, and square root.
At each stage in the construction,
the program calculates a local complex-affine approximation which
contains the class of possible result functions, given
local complex-affine approximation of possible input function(s).

@ The program has a simple structure.
In |verify|, the problem is broken into pieces,
corresponding to strings $p_i$ such that $Z(p_i)$ can be treated
with a single calculation.

|roundoff| discusses the properties of computer arithmetic.

The remainder of the program is presented in reverse order,
starting with the highest-level concepts and ending with the most basic.

|inequalityHolds| uses the specified inequality to prove
that the specified piece is MNG-free.
To do this, it uses two abstractions:
approximate complex $1$-jets (ACJ), and 2x2 matrices of ACJ.

The |SL2ACJ| class reduces operations on matrices of ACJ
to operations on ACJ. It also defines the length and 
ortholength functions and the $s$ and $c$ maps.

The |ACJ| class defines operations on ACJ in terms of operations
on intervals of complex numbers.

The |AComplex| and |XComplex| classes define
operations on intervals of complex numbers.

@*Covering the parameter space.

|verify| pieces together the results of
|inequalityHolds| to cover larger regions.

Codes from the input mean one of three things, as far as |verify| is
concerned.
When $|code| < 0$, |where| is an exceptional case,
to be handled by some other entity, so
|verify| prints |where| and returns.
When $|code| = 0$, |where| is a composite case, so
|verify| calls itself, first on |where0| and then on |where1|.
When $|code| > 0$, |where| is an atomic case,
so |verify| uses |inequalityHolds|
to show that $Z(|where|)$ is MNG-free.
If this isn't possible, |verify| tries the same code
on two parts of |where|.

If |autocode > 0|, then |verify| doesn't read from the input,
and uses |autocode| instead.

\lemma
If |verify(where,depth,code)| finishes, and prints
``$m_0 \dots m_k$'', then
$Z(|where|) - \Union_i Z(m_i)$ is MNG-free.
\endlemma

@<Definition of |verify|@>=
void verify(char* where, int depth, int autocode)
{
  int code;
  if (depth >= MAXDEPTH) {
    where[depth] = '\0';
    fprintf(stderr, "verify: fatal error at %s\n", where);
    exit(1);
  }
  if (autocode == 0) {
    scanf("%d", &code);
  } else {
    code = autocode;
  }
  if (code < 0) {
    where[depth] = '\0';
    printf("%s ", where);
  } else if (code != 0 && inequalityHolds(inequalityFor(code), where, depth)) {
      /* where is MNG-free */
  } else {
    where[depth] = '0';
    verify(where, depth+1, code);
    where[depth] = '1';
    verify(where, depth+1, code);
  }
}

@ Positive codes refer to line numbers in the file ``conditionlist'',
which lists all of the inequalities used, one per line.
Given a code number, |inequalityFor| returns the corresponding inequality
from the file.
The first time it's called,
|inequalityFor| also reads the file into |inequalities|,
and initializes an array of pointers to the beginning of each line.

@<Definition of |inequalityFor|@>=
const char* inequalityFor(int code)
{
  const int max_n_inequalities = 13200;
  const int max_inequalities_size = 300000;
  static int n_inequalities = 0;
  static char inequalities[max_inequalities_size];
  static char* inequalityIndex[max_n_inequalities];
  if (n_inequalities == 0) {
    FILE* fp = fopen("conditionlist", "r");
    if (fp == NULL) {
      fprintf(stderr, "can't open conditionlist\n");
      exit(1);
    }
    int n_read = fread(inequalities, 1, max_inequalities_size, fp);
    char* ip = inequalities;
    n_inequalities = 1;
    inequalityIndex[n_inequalities++] = inequalities;
    while (n_inequalities < max_n_inequalities && ip < inequalities+n_read-1) {
      if (*ip == '\n')
	inequalityIndex[n_inequalities++] = ip+1;
      ip++;
    }
    fclose(fp);
  }
  if (code < 1 || code >= n_inequalities) {
    fprintf(stderr, "code %d out of range [1,%d] in inequalityFor\n",
      code, n_inequalities);
    exit(1);
  }
  return inequalityIndex[code];
}

@ The |main| program is almost trivial.
@<Definition of |main|@>=
main(int argc, char** argv)
{
  if (argc != 2) {
    fprintf(stderr, "Usage: %s position < data\n", argv[0]);
    exit(1);
  }
  char where[MAXDEPTH];
  int depth;
  for (depth = 0; argv[1][depth] != '\0'; depth++) {
    if (argv[1][depth] != '0' && argv[1][depth] != '1') {
      fprintf(stderr, "bad position %s\n", argv[1]);
      exit(1);
    }
    where[depth] = argv[1][depth];
  }
  where[depth] = '\0';

  initialize_roundoff();
  verify(where, depth, 0);
  if (!roundoff_ok()) {
    printf("\n. underflow may have occurred\n");
    exit(1);
  }
  exit(0);
}

@ @<Definition of |MAXDEPTH|@>=
const int MAXDEPTH = 200;

@i roundoff.w
@i Codes.w
@i SL2ACJ.w
@i ACJ.w
@i Complex.w
@i glue.w