plane_depth: add level/interlevel dual edge definitions

Extends Definition 1.2 (level edge) to also define "interlevel edge"
for the primal, and adds Definition 1.3 (level/interlevel dual edge)
classifying dual edges by whether they cross a level or interlevel
primal edge.

Useful downstream: in coloring_nested_tire_graphs, the partial tire
dual's edges can now be classified cleanly as level or interlevel
dual edges using the same vocabulary, instead of ad hoc "interior
annular edge" / "spoke edge" naming.

Paper stays at 4 pages.

Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com>

papers/plane_depth/paper.tex

@@ -76,7 +76,23 @@ $G$.
 \begin{definition}
 \label{def:level-edge}
 An edge $\{u, v\} \in E(G)$ is a \emph{level edge} if
-$\mathrm{depth}(u) = \mathrm{depth}(v)$.
+$\mathrm{depth}(u) = \mathrm{depth}(v)$, and an \emph{interlevel
+edge} if $\mathrm{depth}(u) \neq \mathrm{depth}(v)$.
+\end{definition}
+
+Under planar duality, each primal edge of $G$ corresponds to a
+unique edge of the planar dual --- the edge between the two face
+vertices on either side of the primal edge.  Levels and interlevels
+lift to the dual:
+
+\begin{definition}
+\label{def:level-dual-edge}
+A dual edge of $G$ is a \emph{level dual edge} if it crosses a level
+edge of $G$ in the planar embedding (equivalently, if its
+corresponding primal edge has equal-depth endpoints), and an
+\emph{interlevel dual edge} if it crosses an interlevel edge
+(equivalently, if its corresponding primal edge has
+different-depth endpoints).
 \end{definition}
 
 \begin{definition}