Add contraction-lift proof-strategy sketch toward Conjecture 5.7

Section 5.6 sketches an inductive route to the simple-resolution md4
surjectivity conjecture:

- Lemma 5.8 (good contraction): every md4 triangulation on n >= 7
  vertices has a degree-4 vertex with an md4-preserving diagonal
  contraction. Empirically true at n=7..11; proof obligation called
  out.
- Lemma 5.9 (lift): given a labelled preimage of the contracted
  triangulation, reinserting the contracted vertex at the
  diagonal-bounded quadrilateral yields a preimage of the original
  triangulation. Proof obligation called out.
- Inductive scheme paragraph chains the two lemmas with the octahedron
  at n=6 as the base case, citing the n=7 hand-verification (already
  scripted in experiments/inductive_lift_check.py).

Lemmas are stated without proof; the three remaining proof
obligations are explicit.

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

papers/level_resolutions_of_maximal_planar_graphs/paper.tex

@@ -539,6 +539,102 @@ vertices is not reachable by the algorithm; at $n = 10$, two further
 iso-classes with four degree-$3$ vertices and high-degree hubs fail to
 appear among algorithm outputs.
 
+\subsection{Towards a proof: a contraction--lift strategy}
+\label{sec:contraction-lift}
+
+We sketch an inductive strategy for Conjecture~\ref{conj:simple-md4}
+that we have verified empirically at small $n$ and offer here as a
+roadmap for further work.
+
+Let $T$ be a plane triangulation with minimum degree at least $4$, and
+let $v \in V(T)$ be a degree-$4$ vertex with cyclic neighbors
+$a, b, c, d$ (in the cyclic order inherited from $T$'s planar
+embedding). Removing $v$ from $T$ exposes the $4$-cycle $abcd$, which we
+retriangulate by adding one of the two diagonals $(a, c)$ or $(b, d)$.
+We call this operation \emph{contraction at $v$ along diagonal
+$(a, c)$}, denoted $T_{v, (a, c)}$. The contraction is \emph{valid} when
+the chosen diagonal is not already an edge of $T$.
+
+\begin{lemma}[Good contraction]
+\label{lem:good-contraction}
+Let $T$ be a plane triangulation on $n \geq 7$ vertices with minimum
+degree at least $4$. Then there exist a degree-$4$ vertex $v \in V(T)$,
+with cyclic neighbors $a, b, c, d$, and an unordered pair
+$\{a, c\}$ such that:
+\begin{enumerate}
+\item $(a, c) \not\in E(T)$;
+\item $\deg_T(b) \geq 5$ and $\deg_T(d) \geq 5$.
+\end{enumerate}
+Under these conditions $T_{v, (a, c)}$ is a plane triangulation on
+$n - 1$ vertices with minimum degree at least $4$.
+\end{lemma}
+
+The conditions of Lemma~\ref{lem:good-contraction} ensure that the
+contraction is valid (1) and md$_4$-preserving (2): the only vertices
+whose degree changes under $T \to T_{v, (a, c)}$ are $a, b, c, d$, with
+$\deg(a)$ and $\deg(c)$ unchanged (each loses the edge to $v$ but gains
+the edge from the diagonal), while $\deg(b)$ and $\deg(d)$ each decrease
+by $1$.
+
+The lemma is empirically true at $n = 7, \ldots, 11$ for every md$_4$
+iso-class; we conjecture it holds for all $n \geq 7$. The $n = 6$ case
+is excluded: the unique md$_4$ iso-class is the octahedron, in which
+every vertex has all four cyclic neighbors at degree $4$ and so no
+contraction preserves md$_4$. The octahedron is therefore the base case
+of the proposed induction.
+
+\begin{lemma}[Lift]
+\label{lem:lift}
+Let $T$ be a plane triangulation with minimum degree at least $4$, and
+suppose Lemma~\ref{lem:good-contraction} applies via vertex $v$ and
+diagonal $(a, c)$ with $T_{v, (a, c)}$ the resulting contraction. Let
+$H$ be a plane triangulation on $V(T_{v, (a, c)}) = V(T) \setminus \{v\}$
+and $S$ a level source of $H$ such that the algorithm of
+Section~\ref{sec:flip-algorithm} applied to $(H, S)$ produces
+$T_{v, (a, c)}$ as a labelled simple graph. Define the \emph{lift}
+$G \;:=\; H[a, b, c, d, v]$ by:
+\begin{itemize}
+\item adding vertex $v$ to $V(H)$;
+\item removing the edge $(a, c)$ from $E(H)$;
+\item adding the four edges $(v, a), (v, b), (v, c), (v, d)$.
+\end{itemize}
+Then $G$ is a plane triangulation on $|V(T)|$ vertices, and the
+algorithm of Section~\ref{sec:flip-algorithm} applied to $(G, S)$
+produces $T$.
+\end{lemma}
+
+Lemma~\ref{lem:lift} requires that $(a, c) \in E(H)$ and that the two
+triangles of $H$ bordering $(a, c)$ have boundary
+$\{a, b, c, d\}$. When these conditions hold, the lift restores a
+degree-$4$ vertex $v$ inserted into the quadrilateral $abcd$; when they
+fail, the lift is undefined and a different labelled preimage $H$ must
+be chosen.
+
+\paragraph{Inductive scheme.}
+Conjecture~\ref{conj:simple-md4} would follow from
+Lemmas~\ref{lem:good-contraction} and~\ref{lem:lift} together with the
+existence at each step of a labelled preimage $H$ satisfying the lift's
+side conditions. The base case is the octahedron at $n = 6$, which is
+empirically a simple level resolution
+(Observation~\ref{obs:md4-simple-resolution}). The inductive step takes
+an md$_4$ target $T$ on $n$ vertices, applies
+Lemma~\ref{lem:good-contraction} to obtain an md$_4$ contraction
+$T_{v, (a, c)}$ on $n - 1$ vertices, invokes the inductive hypothesis to
+produce a labelled preimage $H$, and applies Lemma~\ref{lem:lift} to
+lift $H$ to $G$ with $\mathrm{alg}(G, S) = T$.
+
+We have verified the entire scheme by hand for the unique md$_4$
+iso-class at $n = 7$: contraction at $v = 2$ along diagonal $(4, 3)$
+yields the octahedron on six vertices labelled $\{0, 1, 3, 4, 5, 6\}$;
+a labelled preimage $H$ exists with source $S = \{0, 1, 6\}$; lifting
+along $(4, 3, v = 2)$ produces a triangulation $G$ on seven vertices on
+which the algorithm with source $S$ recovers $T$ exactly. The principal
+remaining work is a proof of Lemma~\ref{lem:good-contraction} for all
+$n \geq 7$, a proof of Lemma~\ref{lem:lift} (which involves analysing
+how the algorithm's depth-guided flips interact with the added vertex
+$v$), and a guarantee that a label-faithful preimage $H$ always
+exists.
+
 \begin{question}
 \label{q:terminate-all-n}
 Does Phase~1 terminate for all $(G, S)$? Equivalently, is there an