diff --git a/paper/gtt.tex b/paper/gtt.tex
index 12c744f64a48bbb23e7ffd300e0184bb40e591f8..8059ffdb85b93310e43d38299c8baf79e1c18ca6 100644
--- a/paper/gtt.tex
+++ b/paper/gtt.tex
@@ -1730,9 +1730,55 @@ This makes it slightly harder to establish the intended equivalence $M
 makes the logical relation theorem stronger: it proves that diverging
 terms must use recursive types of some sort and so any term that does
 not use them terminates.
+%
+This issue would be alleviated if we had proved type safety by a
+logical relation rather than by progress and preservation.
+
+However, the following properties of the indexed relation can easily
+be established.
+%
+First a kind of ``transitivity'' of the indexed relation with respect
+to the original preorder, that is key to proving transitivity of the
+logical relation.
+\begin{lemma}{Indexed Relation is a Module of the Preorder}
+  If $M \ix\apreorder i R$ and $R \apreorder R'$ then $M \ix\apreorder i R'$
+\end{lemma}
+\begin{proof}
+  If $M \bigstepsin{i} M'$ then there's nothing to show, otherwise $M
+  \bigstepsin{j< i} \result(M)$ so it follows by transitivity of the
+  preorder: $\result(M) \apreorder R \apreorder R'$.
+\end{proof}
+
+Next, we show the relation is downward-closed
+
+\begin{lemma}{Downward Closure of Indexed Relation}
+  If $M \ix\apreorder i R$ and $j\leq i$ then $M \ix \apreorder j R$.
+\end{lemma}
+\begin{proof}
+  \begin{enumerate}
+  \item If $M \bigstepsin{i} M_i$ then $M \bigstepsin{j} M_j$ and otherwise 
+  \item If $M \bigstepsin{j \leq k i} \result(M)$ then $M \bigstepsin{j} M_j$
+  \item if $M \bigstepsin{k < j \leq i} \result(M)$ then $\result(M) \apreorder R$.
+  \end{enumerate}
+\end{proof}
+
+\begin{lemma}{Triviality at $0$}
+  For any $\cdot \vdash M : \u F 2$, $M \ix\apreorder 0 R$
+\end{lemma}
+\begin{proof}
+  Because $M \bigstepsin{0} M$
+\end{proof}
 
-% TODO: pole properties go here: down-closed, trivial at 0, indexed
-% anti-reduction (transitivity is later, error awareness is trivial!)
+\begin{lemma}{Anti-reduction}
+  If $M \ix\apreorder i R$ and $N \bigstepsin{j} M$, then $N \ix\apreorder {i+j} R$
+\end{lemma}
+\begin{proof}
+  \begin{enumerate}
+  \item If $M \bigstepsin{i} M'$ then $N \bigstepsin{i+j} M'$
+  \item If $M \bigstepsin{k < i} \result(M)$ then $N \bigstepsin{k+j < i+j}
+    \result(M)$ and $\result(M) = \result(N)$.
+  \end{enumerate}
+\end{proof}
 
 Next, we define the \emph{logical} preorder by induction on types and
 the index $i$ in figure \ref{lr}.
@@ -1773,8 +1819,14 @@ Next, analogous to the contextual preorder, we define the
 We next want to prove that the logical preorder is a congruence
 relation, i.e., the fundamental lemma of the logical relation.
 
-% TODO: downward closure lemma
-
+\begin{lemma}{Logical Relation Downward Closure}
+  \begin{enumerate}
+  \item If $V_1 \ilrof\apreorder i A V_2$ and $j\leq i$ then $V_1
+    \ilrof\apreorder j A V_2$
+  \item If $S_1 \ilrof\apreorder i {\u B} S_2$ and $j\leq i$ then $S_1
+    \ilrof\apreorder j {\u B} S_2$
+  \end{enumerate}
+\end{lemma}
 \begin{theorem}{Logical Preorder is a Congruence}
   For any preorder on results with diverge least element, the logical
   preorder $\ilrof\apreorder i {}$ is a congruence relation, i.e.,
@@ -1786,10 +1838,117 @@ relation, i.e., the fundamental lemma of the logical relation.
 
 \begin{corollary}{Reflexivity}
   For any $\Gamma \vdash M : \u B$, and $i \in \mathbb{N}$,
-  \[\Gamma \vDash M \ilorof\apreorder i {} M \in \u B.\]
+  \[\Gamma \vDash M \ilrof\apreorder i {} M \in \u B.\]
+\end{corollary}
+
+As another corollary we have the following \emph{strengthening} of the
+progress-and-preservation type soundness theorem because it only
+counts unrolling steps.
+\begin{corollary}{Unary LR}
+  For every program $\cdot \vdash M : \u F 2$, \[ M \ix\apreorder i \result(M) \]
 \end{corollary}
+\begin{proof}
+  By reflexivity, $\cdot \vDash M \ix\apreorder i M \in \u F 2$ and by
+  definition $\bullet \ilrof\apreorder i {\u F 2} \bullet$, so
+  unrolling definitions we get $M \ix\apreorder i \result(M)$.  
+\end{proof}
 
-% Corollary: relation in the limit recovers the original ordering!
+Using the reflexivity proof, we can now prove that the indexed
+relation between terms and results recovers the original preorder in
+the limit as $i \to \infty$.
+\begin{corollary}{In the limit, Finitized Preorder Recovers Original}
+  For any preorder with divergence-least element $\apreorder$,
+  \[ \result(M) \apreorder R \iff \forall i \in \mathbb{N}.~ M \ix\apreorder i R \]
+\end{corollary}
+\begin{proof}
+  Two cases
+  \begin{enumerate}
+  \item If $\result(M) \apreorder R$ then we need to show for every $i
+    \in \mathbb{N}$, $M \ix \apreorder i R$. First, by lemma above, $M
+    \ix\apreorder i \result(M)$, so we do a case analysis
+    \begin{enumerate}
+    \item If $M \bigstepsin{i} M'$, then $M \ix\apreorder R$
+    \item If $M \bigstepsin{j<i} R_M$, then $R_M = \result(M)$, so by
+      assumption $R_M \apreorder R$.
+    \end{enumerate}
+  \item If $M \ix\apreorder i R$ for every $i$, then there are two
+    possibilities: $M$ terminates or it doesn't:
+    \begin{enumerate}
+    \item If $M \bigstepsin{i} M_i$ for every $i \in \mathbb{N}$, then
+      $\result(M) = \diverge$ so by assumption that $\diverge$ is a
+      least element, $\result(M) \apreorder R$
+    \item Otherwise there exists some $i \in \mathbb{M}$ such that $M
+      \bigstepsin{i} \result(M)$ and $\result(M) \apreorder R$, in
+      which case there is nothing to show.
+    \end{enumerate}
+  \end{enumerate}
+\end{proof}
+
+With the reflexivity and limiting lemmas in hand, we can prove that
+all of our logical relations (open and closed) are transitive in the
+limit. To do this, we first prove the following kind of
+``quantitative'' transitivity lemma, and then transitivity in the
+limit is a consequence.
+\begin{lemma}{Logical Relation is Quantitatively Transitive}
+  First, for closed terms
+  \begin{enumerate}
+  \item If $V_1 \ilrof\apreorder i A V_2$ and $V_2 \ilrof\apreorder
+    \omega A V_3$, then $V_1 \ilrof\apreorder i A V_3$
+  \item If $S_1 \ilrof\apreorder i {\u B} S_2$ and $S_2 \ilrof\apreorder
+    \omega {\u B} S_3$, then $S_1 \ilrof\apreorder i {\u B} S_3$
+  \end{enumerate}
+
+  Then for open terms
+  \begin{enumerate}
+  \item If $\Gamma \vDash M_1 \ilrof\apreorder i {} M_2 \in \u B$ and
+    $\Gamma \vDash M_2 \ilrof\apreorder \omega {} M_3 \in \u B$, then
+    $\Gamma \vDash M_1 \ilrof\apreorder i {} M_3 \in \u B$.
+  \item If $\Gamma \vDash V_1 \ilrof\apreorder i {} V_2 \in A$ and
+    $\Gamma \vDash V_2 \ilrof\apreorder \omega {} V_3 \in A$, then
+    $\Gamma \vDash V_1 \ilrof\apreorder i {} V_3 \in A$.
+  \item If $\Gamma \pipe \bullet : \u B \vDash S_1 \ilrof\apreorder i {} S_2 \in \u B'$ and
+    $\Gamma\pipe \bullet : \u B \vDash S_2 \ilrof\apreorder \omega {} S_3 \in \u B'$, then
+    $\Gamma\pipe \bullet : \u B \vDash S_1 \ilrof\apreorder i {} S_3 \in \u B'$.
+  \end{enumerate}
+\end{lemma}
+\begin{proof}
+  TODO: adapt from below
+\end{proof}
+
+\begin{corollary}{Logical Relation is Transitive in the Limit}
+  First, for closed terms
+  \begin{enumerate}
+  \item If $V_1 \ilrof\apreorder \omega A V_2$ and $V_2 \ilrof\apreorder
+    \omega A V_3$, then $V_1 \ilrof\apreorder \omega A V_3$
+  \item If $S_1 \ilrof\apreorder \omega {\u B} S_2$ and $S_2 \ilrof\apreorder
+    \omega {\u B} S_3$, then $S_1 \ilrof\apreorder \omega {\u B} S_3$
+  \end{enumerate}
+
+  Then for open terms
+  \begin{enumerate}
+  \item If $\Gamma \vDash M_1 \ilrof\apreorder \omega {} M_2 \in \u B$ and
+    $\Gamma \vDash M_2 \ilrof\apreorder \omega {} M_3 \in \u B$, then
+    $\Gamma \vDash M_1 \ilrof\apreorder \omega {} M_3 \in \u B$.
+  \item If $\Gamma \vDash V_1 \ilrof\apreorder \omega {} V_2 \in A$ and
+    $\Gamma \vDash V_2 \ilrof\apreorder \omega {} V_3 \in A$, then
+    $\Gamma \vDash V_1 \ilrof\apreorder \omega {} V_3 \in A$.
+  \item If $\Gamma \pipe \bullet : \u B \vDash S_1 \ilrof\apreorder \omega {} S_2 \in \u B'$ and
+    $\Gamma\pipe \bullet : \u B \vDash S_2 \ilrof\apreorder \omega {} S_3 \in \u B'$, then
+    $\Gamma\pipe \bullet : \u B \vDash S_1 \ilrof\apreorder \omega {} S_3 \in \u B'$.
+  \end{enumerate}
+\end{corollary}
+
+\begin{lemma}{$\beta, \eta$ Laws are valid}
+  For any preorder with diverge a least element, the $\beta, \eta$
+  laws are valid for $\ilrof\apreorder \omega {}$
+\end{lemma}
+\begin{proof}
+  TODO, easy
+\end{proof}
+
+\begin{lemma}{Substitution Principles}
+  TODO
+\end{lemma}
 
 % Lemma: relation is a module of the ordering/infinite relation
 
@@ -1826,7 +1985,7 @@ relation, i.e., the fundamental lemma of the logical relation.
       S_1 \logty i {\u F A} S_2 & = & \forall j\leq i, V_1 \logty j A V_2.~ S_1[\ret V_1] \logc j S_2[\ret V_2]
     \end{array}
   \end{mathpar}
-  \caption{Observational Error Approximation Logical Relation}
+  \caption{Logical Relation from a Preorder $\apreorder$}
 \end{figure}
 
 \begin{definition}[Pole]