Prove intertwining-tree ⟺ Hamiltonian-dual; test the 6 Holton-McKay duals

- Add Theorem: maximal planar G is an intertwining tree iff its dual
  G* is Hamiltonian (Tait-style Jordan-curve argument). Consequence:
  smallest non-intertwining-tree triangulations are the 6 duals of the
  38-vertex Holton-McKay graphs, at n=21.
- Load the 6 graphs from McKay's authoritative planar_code file
  (nonham38m4.pc), verified: 38 vertices, cubic, planar, non-Hamiltonian.
- All 6 duals confirmed not intertwining trees (exhaustive 2^20 check).
- 2 of 6 duals are themselves Even Level Graphs (sources 9, 10), hence
  derived level graphs -- first cases where the derived disjunct does
  work the intertwining-tree disjunct cannot.
- Remaining 4: bounded E/O-orbit search inconclusive; status open. This
  is the first genuinely undetermined instance of the conjecture.

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

papers/even_level_graph_generators/paper.tex

@@ -257,12 +257,47 @@ vertex set can be partitioned into two sets $A$ and $B$ such that
 both induced subgraphs $G[A]$ and $G[B]$ are trees.
 \end{definition}
 
+\begin{theorem}
+\label{thm:intertwining-iff-hamiltonian-dual}
+A maximal planar graph $G$ is an intertwining tree if and only if its
+dual $G^\ast$ has a Hamiltonian cycle.
+\end{theorem}
+
+\begin{proof}
+($\Rightarrow$) Let $V(G) = A \sqcup B$ with $G[A]$ and $G[B]$ trees.
+Every triangular face $\{x,y,z\}$ of $G$ meets both $A$ and $B$: if all
+three vertices were in $A$ the triangle would be a cycle in the tree
+$G[A]$, and likewise for $B$. Draw a closed curve through the faces of
+$G$ separating the $A$-vertices from the $B$-vertices within each face.
+Since every face is split, the curve visits every face exactly once and
+crosses an edge of $G$ precisely when that edge joins $A$ to $B$; it is
+therefore a Hamiltonian cycle of $G^\ast$.
+
+($\Leftarrow$) Let $H$ be a Hamiltonian cycle of $G^\ast$. Drawn in the
+plane, $H$ is a Jordan curve visiting every face of $G$ once; let $A$
+and $B$ be the vertices of $G$ interior and exterior to $H$. The
+$2n-4$ edges of $H$ cross exactly the edges of $G$ between $A$ and $B$,
+leaving $(3n-6)-(2n-4) = n-2$ edges inside $G[A]$ and $G[B]$ together.
+The edges inside $A$ lie in the disk bounded by $H$ and span $A$
+without enclosing a face (each face is cut by $H$), so $G[A]$ is a tree;
+likewise $G[B]$.
+\end{proof}
+
 \begin{conjecture}
 \label{conj:every-triangulation-derived}
 Every maximal planar graph is a valid derived level graph of some Even
 Level Graph, an intertwining tree, or both.
 \end{conjecture}
 
+By Theorem~\ref{thm:intertwining-iff-hamiltonian-dual}, the
+intertwining-tree disjunct fails for $G$ exactly when $G^\ast$ is a
+counterexample to Tait's conjecture. The smallest such $G^\ast$ have
+$38$ vertices (Holton--McKay~\cite{holton-mckay}, exactly $6$ graphs),
+so the smallest triangulations that are not intertwining trees occur at
+$n = 21$ and there are exactly $6$ of them. Below $n = 21$ every
+maximal planar graph is an intertwining tree, which is why the
+disjunction holds trivially in that range.
+
 \subsection*{Empirical status}
 
 For each isomorphism class of maximal planar graphs on $n$ vertices,
@@ -284,4 +319,43 @@ $12$ & $7595$ & $0$ & $1$ & $7594$ & $0$ & holds \\
 \end{tabular}
 \end{center}
 
+\subsection*{The boundary case $n = 21$}
+
+The first triangulations that are \emph{not} intertwining trees are the
+six duals of the Holton--McKay graphs, at $n = 21$. For the disjunction
+to survive at $n = 21$, each of these six must be a valid derived level
+graph. We find:
+\begin{itemize}
+\item All six duals are confirmed not intertwining trees (exhaustive
+check of all $2^{20}-1$ vertex bipartitions), consistent with
+Theorem~\ref{thm:intertwining-iff-hamiltonian-dual}.
+\item Two of the six are themselves Even Level Graphs (for a suitable
+source vertex), hence trivially valid derived level graphs. So the
+disjunction holds for them through the derived-level-graph disjunct --
+the first instances where that disjunct does work the intertwining-tree
+disjunct cannot.
+\item The remaining four are not Even Level Graphs for any source. A
+bounded backward $E/O$-orbit search (tens of thousands of states, a
+handful of source labellings) found no Even Level Graph in their
+orbits, but this is far too shallow relative to the orbit size at
+$n = 21$ to be conclusive; their status as derived level graphs is
+open.
+\end{itemize}
+Thus at $n = 21$ the disjunction is confirmed for two of the six
+critical iso classes and undetermined for the other four. Settling
+those four -- equivalently, deciding $E/O$-orbit reachability from an
+Even Level Graph -- is the first genuinely open instance of the
+conjecture, and calls for either a better reachability algorithm or a
+structural invariant of $E/O$-orbits.
+
+\begin{thebibliography}{9}
+
+\bibitem{holton-mckay}
+D.~A. Holton and B.~D. McKay.
+\emph{The smallest non-Hamiltonian 3-connected cubic planar graphs have
+38 vertices}.
+Journal of Combinatorial Theory, Series B, 45(3):305--319, 1988.
+
+\end{thebibliography}
+
 \end{document}