Add neutral triangle definition and use up/down/neutral triangle terms in lemma

Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com>

papers/plane_depth_sequencing/paper.fdb_latexmk

@@ -1,6 +1,6 @@
 # Fdb version 4
-["pdflatex"] 1777104409.51711 "/home/didericis/Code/math-research/papers/plane_depth_sequencing/paper.tex" "paper.pdf" "paper" 1777104409.7899 0
-  "/home/didericis/Code/math-research/papers/plane_depth_sequencing/paper.tex" 1777104409.33562 5020 563243a3090f17940469736cc026af9c ""
+["pdflatex"] 1777104894.61083 "/home/didericis/Code/math-research/papers/plane_depth_sequencing/paper.tex" "paper.pdf" "paper" 1777104894.88704 0
+  "/home/didericis/Code/math-research/papers/plane_depth_sequencing/paper.tex" 1777104894.41564 5298 4a3acc81f8f9c682ff322e02fe18ccf7 ""
   "/nix/store/4g7bv3lsd1r7lrfxi0x145xac0jag4hl-texlive-combined-full-2025.20250703/share/texmf-var/fonts/map/pdftex/updmap/pdftex.map" 1 5523663 ec1f96d89b308e150332b305019a3402 ""
   "/nix/store/4g7bv3lsd1r7lrfxi0x145xac0jag4hl-texlive-combined-full-2025.20250703/share/texmf-var/web2c/pdftex/pdflatex.fmt" 1 3600504 177ced77725200f4fa24b79427ded12f ""
   "/nix/store/4g7bv3lsd1r7lrfxi0x145xac0jag4hl-texlive-combined-full-2025.20250703/share/texmf-var/web2c/texmf.cnf" 1 44455 00ca67f5a06c9c23b32559f3f48cb4e9 ""
@@ -45,8 +45,8 @@
   "/nix/store/zwvq8i154s539b4w2fqhia83fsfng7ng-texlive-combined-full-2025.20250703-texmfdist/tex/latex/amsmath/amsopn.sty" 1 4474 c510a88aa5f51b8c773b50a7ee92befd ""
   "/nix/store/zwvq8i154s539b4w2fqhia83fsfng7ng-texlive-combined-full-2025.20250703-texmfdist/tex/latex/amsmath/amstext.sty" 1 2444 9983e1d0683f102e3b190c64a49313aa ""
   "/nix/store/zwvq8i154s539b4w2fqhia83fsfng7ng-texlive-combined-full-2025.20250703-texmfdist/tex/latex/l3backend/l3backend-pdftex.def" 1 30351 a2b09edc6c93a742566b222c33d0278e ""
-  "paper.aux" 1777104409.75063 278 6ee4d5d6b3925666e01309d058e35079 "pdflatex"
-  "paper.tex" 1777104409.33562 5020 563243a3090f17940469736cc026af9c ""
+  "paper.aux" 1777104894.84465 278 6ee4d5d6b3925666e01309d058e35079 "pdflatex"
+  "paper.tex" 1777104894.41564 5298 4a3acc81f8f9c682ff322e02fe18ccf7 ""
   (generated)
   "paper.aux"
   "paper.log"

papers/plane_depth_sequencing/paper.log

@@ -1,4 +1,4 @@
-This is pdfTeX, Version 3.141592653-2.6-1.40.27 (TeX Live 2025/nixos.org) (preloaded format=pdflatex 1980.1.1)  25 APR 2026 04:07
+This is pdfTeX, Version 3.141592653-2.6-1.40.27 (TeX Live 2025/nixos.org) (preloaded format=pdflatex 1980.1.1)  25 APR 2026 04:15
 entering extended mode
  restricted \write18 enabled.
  %&-line parsing enabled.
@@ -178,11 +178,11 @@ L3 programming layer <2025-06-09>
 Here is how much of TeX's memory you used:
  1763 strings out of 467888
  25768 string characters out of 5405403
- 436018 words of memory out of 5000000
+ 435018 words of memory out of 5000000
  30194 multiletter control sequences out of 15000+600000
  633232 words of font info for 65 fonts, out of 8000000 for 9000
  1302 hyphenation exceptions out of 8191
- 71i,6n,79p,751b,238s stack positions out of 10000i,1000n,20000p,200000b,200000s
+ 71i,6n,79p,751b,236s stack positions out of 10000i,1000n,20000p,200000b,200000s
 </nix/store/zwvq8i154s539b4w2fqhia83fsfng7ng-texlive-combined-full-2025.20250
 703-texmfdist/fonts/type1/public/amsfonts/cm/cmbx10.pfb></nix/store/zwvq8i154s5
 39b4w2fqhia83fsfng7ng-texlive-combined-full-2025.20250703-texmfdist/fonts/type1
@@ -204,7 +204,7 @@ i154s539b4w2fqhia83fsfng7ng-texlive-combined-full-2025.20250703-texmfdist/fonts
 /type1/public/amsfonts/cm/cmti8.pfb></nix/store/zwvq8i154s539b4w2fqhia83fsfng7n
 g-texlive-combined-full-2025.20250703-texmfdist/fonts/type1/public/amsfonts/sym
 bols/msam10.pfb>
-Output written on paper.pdf (2 pages, 143149 bytes).
+Output written on paper.pdf (2 pages, 144144 bytes).
 PDF statistics:
  71 PDF objects out of 1000 (max. 8388607)
  42 compressed objects within 1 object stream

papers/plane_depth_sequencing/paper.tex

@@ -90,6 +90,10 @@ where $d(v, u)$ denotes the graph distance between $v$ and $u$ in $G$.
 An edge $\{u, v\} \in E(G)$ is a \emph{level edge} if $\mathrm{depth}(u) = \mathrm{depth}(v)$.
 \end{definition}
 
+\begin{definition}
+A triangle $\{u, v, w\}$ in $G$ is an \emph{up triangle} if the multiset of depths of its vertices is $\{d, d+1, d+1\}$ for some $d \geq 0$, a \emph{down triangle} if the multiset of depths is $\{d, d, d+1\}$ for some $d \geq 0$, and a \emph{neutral triangle} if the multiset of depths is $\{d, d, d\}$ for some $d \geq 0$.
+\end{definition}
+
 \begin{definition}
 Let $G$ be a maximal planar graph with a plane embedding and outer cycle $C$. The \emph{deep embedding} of $G$ is the graph $G'$ obtained from $G$ by the following operation: for every 3-cycle $\{u, v, w\} \subseteq V(G)$ such that
 \[
@@ -99,19 +103,19 @@ add a new vertex $x$ to $G$ adjacent to each of $u$, $v$, and $w$.
 \end{definition}
 
 \begin{lemma}
-Let $G'$ be the deep embedding of a maximal planar graph $G$. For each face of $G'$, the plane depths of its three vertices are either $d, d+1, d+1$ or $d, d, d+1$ for some $d \geq 0$.
+Let $G'$ be the deep embedding of a maximal planar graph $G$. Every face of $G'$ is either an up triangle or a down triangle.
 \end{lemma}
 
 \begin{proof}
 We first establish that for any edge $\{p, q\}$ in $G$, the depths of $p$ and $q$ differ by at most $1$. Suppose for contradiction that $\mathrm{depth}(p) = d$ and $\mathrm{depth}(q) = d + n$ for some $n \geq 2$. Since $\mathrm{depth}(p) = d$, there exists a path of length $d$ from $p$ to some vertex of $C$. Prepending the edge $\{q, p\}$ gives a path of length $d + 1$ from $q$ to $C$, so $\mathrm{depth}(q) \leq d + 1 < d + n$, a contradiction. The case $\mathrm{depth}(q) = d - n$ is handled identically: there exists a path of length $d - n$ from $q$ to some vertex of $C$, and prepending the edge $\{p, q\}$ gives a path of length $d - n + 1 \leq d - 1 < d$ from $p$ to $C$, contradicting $\mathrm{depth}(p) = d$.
 
-Since $G$ is a triangulation, every interior face of $G$ is a triangle $\{u,v,w\}$ with all three pairs adjacent. By the above, each pair of vertices in a triangle differs in depth by at most $1$, so no triangle can contain vertices of depths $d$ and $d+2$ simultaneously. The possible depth patterns for a triangle in $G$ are therefore exactly $d,d,d$, or $d,d,d+1$, or $d,d+1,d+1$.
+Since $G$ is a triangulation, every interior face of $G$ is a triangle $\{u,v,w\}$ with all three pairs adjacent. By the above, each pair of vertices in a triangle differs in depth by at most $1$, so no triangle can contain vertices of depths $d$ and $d+2$ simultaneously. The possible depth patterns for a triangle in $G$ are therefore exactly a neutral triangle, a down triangle, or an up triangle.
 
 We now consider each case under the deep embedding.
 
-\textit{Case 1: depths $d,d,d+1$ or $d,d+1,d+1$.} These triangles are not modified by the deep embedding, so they remain as faces of $G'$ with the stated depth patterns, satisfying the lemma.
+\textit{Case 1: up triangle or down triangle.} These triangles are not modified by the deep embedding, so they remain as faces of $G'$, satisfying the lemma.
 
-\textit{Case 2: depths $d,d,d$.} The deep embedding inserts a new vertex $x$ adjacent to $u$, $v$, and $w$, replacing the face $\{u,v,w\}$ with three new faces $\{u,v,x\}$, $\{v,w,x\}$, and $\{u,w,x\}$. It remains to determine the depth of $x$ in $G'$. Since $x$ is adjacent only to $u$, $v$, and $w$, every path in $G'$ from $x$ to $C$ must pass through one of them, so $x$ has strictly greater depth than $u$, $v$, and $w$. Each of the three new faces thus has depth pattern $d,d,d+1$, satisfying the lemma.
+\textit{Case 2: neutral triangle.} The deep embedding inserts a new vertex $x$ adjacent to $u$, $v$, and $w$, replacing the face $\{u,v,w\}$ with three new faces $\{u,v,x\}$, $\{v,w,x\}$, and $\{u,w,x\}$. It remains to determine the depth of $x$ in $G'$. Since $x$ is adjacent only to $u$, $v$, and $w$, every path in $G'$ from $x$ to $C$ must pass through one of them, so $x$ has strictly greater depth than $u$, $v$, and $w$. Each of the three new faces is thus a down triangle, satisfying the lemma.
 
 Since every face of $G'$ falls into one of these cases, the result follows.
 \end{proof}