chore: SAVEPOINT

This commit is contained in:
2026-04-13 11:01:31 -04:00
parent 3098347da2
commit ada26b6801
7 changed files with 249 additions and 20 deletions
+16 -3
View File
@@ -1,7 +1,20 @@
\relax
\@writefile{toc}{\contentsline {section}{\tocsection {}{1}{Kempe's Proof (Valid Portion)}}{1}{}\protected@file@percent }
\@writefile{toc}{\contentsline {subsection}{\tocsubsection {}{1.1}{Setup}}{1}{}\protected@file@percent }
\@writefile{toc}{\contentsline {subsection}{\tocsubsection {}{1.2}{Every Planar Graph Has a Vertex of Degree at Most 5}}{1}{}\protected@file@percent }
\@writefile{toc}{\contentsline {subsection}{\tocsubsection {}{1.3}{Cases of Degree at Most 3}}{1}{}\protected@file@percent }
\@writefile{toc}{\contentsline {subsection}{\tocsubsection {}{1.4}{Case of Degree 4}}{2}{}\protected@file@percent }
\@writefile{toc}{\contentsline {section}{\tocsection {}{2}{Resolution of Degree 5 Case}}{2}{}\protected@file@percent }
\@writefile{toc}{\contentsline {subsection}{\tocsubsection {}{2.1}{At Least 12 Vertices of Degree 5}}{2}{}\protected@file@percent }
\@writefile{toc}{\contentsline {subsection}{\tocsubsection {}{2.2}{Two Non-Adjacent Vertices of Degree 5}}{3}{}\protected@file@percent }
\@writefile{toc}{\contentsline {subsection}{\tocsubsection {}{2.3}{The Reduced Subgraph $G'$}}{3}{}\protected@file@percent }
\@writefile{toc}{\contentsline {subsection}{\tocsubsection {}{2.4}{Not All Colorings in $\Phi $ Saturate Both Neighborhoods}}{3}{}\protected@file@percent }
\@writefile{toc}{\contentsline {section}{\tocsection {}{3}{Merged Subgraphs of $G'$}}{3}{}\protected@file@percent }
\newlabel{tocindent-1}{0pt}
\newlabel{tocindent0}{0pt}
\newlabel{tocindent1}{0pt}
\newlabel{tocindent2}{0pt}
\newlabel{tocindent1}{17.77782pt}
\newlabel{tocindent2}{29.38873pt}
\newlabel{tocindent3}{0pt}
\gdef \@abspage@last{1}
\@writefile{toc}{\contentsline {subsection}{\tocsubsection {}{3.1}{Colorings of Merged Subgraphs Extend to $G'$}}{4}{}\protected@file@percent }
\@writefile{toc}{\contentsline {subsection}{\tocsubsection {}{3.2}{4-Saturating Merged Colorings Extend to 4-Saturating Colorings of $G'$}}{4}{}\protected@file@percent }
\gdef \@abspage@last{4}
+16 -4
View File
@@ -1,6 +1,6 @@
# Fdb version 3
["pdflatex"] 1776046763 "/Users/didericis/Code/magnum-opus-4ct/paper.tex" "paper.pdf" "paper" 1776046763
"/Users/didericis/Code/magnum-opus-4ct/paper.tex" 1776046763 2179 8055ca3cd1baeac7b377564e439027b4 ""
["pdflatex"] 1776052801 "/Users/didericis/Code/magnum-opus-4ct/paper.tex" "paper.pdf" "paper" 1776052801
"/Users/didericis/Code/magnum-opus-4ct/paper.tex" 1776052800 13483 66b66eccf22ca3f14d4a88ccbcab3f5d ""
"/usr/local/texlive/2022/texmf-dist/fonts/map/fontname/texfonts.map" 1577235249 3524 cb3e574dea2d1052e39280babc910dc8 ""
"/usr/local/texlive/2022/texmf-dist/fonts/tfm/public/amsfonts/cmextra/cmex7.tfm" 1246382020 1004 54797486969f23fa377b128694d548df ""
"/usr/local/texlive/2022/texmf-dist/fonts/tfm/public/amsfonts/cmextra/cmex8.tfm" 1246382020 988 bdf658c3bfc2d96d3c8b02cfc1c94c20 ""
@@ -18,14 +18,26 @@
"/usr/local/texlive/2022/texmf-dist/fonts/tfm/public/cm/cmr8.tfm" 1136768653 1292 21c1c5bfeaebccffdb478fd231a0997d ""
"/usr/local/texlive/2022/texmf-dist/fonts/tfm/public/cm/cmsy6.tfm" 1136768653 1116 933a60c408fc0a863a92debe84b2d294 ""
"/usr/local/texlive/2022/texmf-dist/fonts/tfm/public/cm/cmsy8.tfm" 1136768653 1120 8b7d695260f3cff42e636090a8002094 ""
"/usr/local/texlive/2022/texmf-dist/fonts/tfm/public/cm/cmti10.tfm" 1136768653 1480 aa8e34af0eb6a2941b776984cf1dfdc4 ""
"/usr/local/texlive/2022/texmf-dist/fonts/tfm/public/cm/cmti8.tfm" 1136768653 1504 1747189e0441d1c18f3ea56fafc1c480 ""
"/usr/local/texlive/2022/texmf-dist/fonts/tfm/public/cm/cmtt8.tfm" 1136768653 768 d7b9a2629a0c353102ad947dc9221d49 ""
"/usr/local/texlive/2022/texmf-dist/fonts/type1/public/amsfonts/cm/cmbx10.pfb" 1248133631 34811 78b52f49e893bcba91bd7581cdc144c0 ""
"/usr/local/texlive/2022/texmf-dist/fonts/type1/public/amsfonts/cm/cmcsc10.pfb" 1248133631 32001 6aeea3afe875097b1eb0da29acd61e28 ""
"/usr/local/texlive/2022/texmf-dist/fonts/type1/public/amsfonts/cm/cmex10.pfb" 1248133631 30251 6afa5cb1d0204815a708a080681d4674 ""
"/usr/local/texlive/2022/texmf-dist/fonts/type1/public/amsfonts/cm/cmmi10.pfb" 1248133631 36299 5f9df58c2139e7edcf37c8fca4bd384d ""
"/usr/local/texlive/2022/texmf-dist/fonts/type1/public/amsfonts/cm/cmmi7.pfb" 1248133631 36281 c355509802a035cadc5f15869451dcee ""
"/usr/local/texlive/2022/texmf-dist/fonts/type1/public/amsfonts/cm/cmr10.pfb" 1248133631 35752 024fb6c41858982481f6968b5fc26508 ""
"/usr/local/texlive/2022/texmf-dist/fonts/type1/public/amsfonts/cm/cmr5.pfb" 1248133631 31809 8670ca339bf94e56da1fc21c80635e2a ""
"/usr/local/texlive/2022/texmf-dist/fonts/type1/public/amsfonts/cm/cmr7.pfb" 1248133631 32762 224316ccc9ad3ca0423a14971cfa7fc1 ""
"/usr/local/texlive/2022/texmf-dist/fonts/type1/public/amsfonts/cm/cmr8.pfb" 1248133631 32726 0a1aea6fcd6468ee2cf64d891f5c43c8 ""
"/usr/local/texlive/2022/texmf-dist/fonts/type1/public/amsfonts/cm/cmsy10.pfb" 1248133631 32569 5e5ddc8df908dea60932f3c484a54c0d ""
"/usr/local/texlive/2022/texmf-dist/fonts/type1/public/amsfonts/cm/cmsy5.pfb" 1248133631 32915 7bf7720c61a5b3a7ff25b0964421c9b6 ""
"/usr/local/texlive/2022/texmf-dist/fonts/type1/public/amsfonts/cm/cmsy7.pfb" 1248133631 32716 08e384dc442464e7285e891af9f45947 ""
"/usr/local/texlive/2022/texmf-dist/fonts/type1/public/amsfonts/cm/cmti10.pfb" 1248133631 37944 359e864bd06cde3b1cf57bb20757fb06 ""
"/usr/local/texlive/2022/texmf-dist/fonts/type1/public/amsfonts/cm/cmti8.pfb" 1248133631 35660 fb24af7afbadb71801619f1415838111 ""
"/usr/local/texlive/2022/texmf-dist/fonts/type1/public/amsfonts/cm/cmtt8.pfb" 1248133631 24287 6b803fa9eb1ddff9112e00519b09dd9e ""
"/usr/local/texlive/2022/texmf-dist/fonts/type1/public/amsfonts/symbols/msam10.pfb" 1248133631 31764 459c573c03a4949a528c2cc7f557e217 ""
"/usr/local/texlive/2022/texmf-dist/fonts/type1/public/amsfonts/symbols/msbm10.pfb" 1248133631 34694 ad62b13721ee8eda1dcc8993c8bd7041 ""
"/usr/local/texlive/2022/texmf-dist/tex/latex/amscls/amsart.cls" 1591045760 61881 a7369c346c2922a758ae6283cc1ed014 ""
"/usr/local/texlive/2022/texmf-dist/tex/latex/amsfonts/amsfonts.sty" 1359763108 5949 3f3fd50a8cc94c3d4cbf4fc66cd3df1c ""
"/usr/local/texlive/2022/texmf-dist/tex/latex/amsfonts/umsa.fd" 1359763108 961 6518c6525a34feb5e8250ffa91731cff ""
@@ -40,8 +52,8 @@
"/usr/local/texlive/2022/texmf-var/fonts/map/pdftex/updmap/pdftex.map" 1647878959 4410336 7d30a02e9fa9a16d7d1f8d037ba69641 ""
"/usr/local/texlive/2022/texmf-var/web2c/pdftex/pdflatex.fmt" 1665017617 2826443 7e98410c533054b636c6470db83a27bc ""
"/usr/local/texlive/2022/texmf.cnf" 1647878952 577 209b46be99c9075fd74d4c0369380e8c ""
"paper.aux" 1776046763 168 23aeeb56264b611b42959e54d96db7ab "pdflatex"
"paper.tex" 1776046763 2179 8055ca3cd1baeac7b377564e439027b4 ""
"paper.aux" 1776052801 1899 6f6c9f990e281a7651f9bbdc326c1739 "pdflatex"
"paper.tex" 1776052800 13483 66b66eccf22ca3f14d4a88ccbcab3f5d ""
(generated)
"paper.aux"
"paper.log"
+19 -1
View File
@@ -135,13 +135,31 @@ INPUT /usr/local/texlive/2022/texmf-dist/fonts/tfm/public/amsfonts/symbols/msbm5
INPUT /usr/local/texlive/2022/texmf-dist/fonts/tfm/public/cm/cmcsc10.tfm
INPUT /usr/local/texlive/2022/texmf-dist/fonts/tfm/public/cm/cmti8.tfm
INPUT /usr/local/texlive/2022/texmf-dist/fonts/tfm/public/cm/cmbx10.tfm
INPUT /usr/local/texlive/2022/texmf-dist/fonts/tfm/public/cm/cmtt8.tfm
INPUT /usr/local/texlive/2022/texmf-dist/fonts/tfm/public/cm/cmcsc10.tfm
INPUT /usr/local/texlive/2022/texmf-dist/fonts/tfm/public/cm/cmti10.tfm
INPUT /usr/local/texlive/2022/texmf-dist/fonts/tfm/public/amsfonts/cmextra/cmex7.tfm
INPUT /usr/local/texlive/2022/texmf-dist/fonts/tfm/public/amsfonts/symbols/msam10.tfm
INPUT /usr/local/texlive/2022/texmf-dist/fonts/tfm/public/amsfonts/symbols/msam7.tfm
INPUT /usr/local/texlive/2022/texmf-dist/fonts/tfm/public/amsfonts/symbols/msbm10.tfm
INPUT /usr/local/texlive/2022/texmf-dist/fonts/tfm/public/amsfonts/symbols/msbm7.tfm
OUTPUT paper.pdf
INPUT /usr/local/texlive/2022/texmf-var/fonts/map/pdftex/updmap/pdftex.map
INPUT /usr/local/texlive/2022/texmf-dist/fonts/tfm/public/cm/cmtt8.tfm
INPUT paper.aux
INPUT /usr/local/texlive/2022/texmf-dist/fonts/type1/public/amsfonts/cm/cmbx10.pfb
INPUT /usr/local/texlive/2022/texmf-dist/fonts/type1/public/amsfonts/cm/cmcsc10.pfb
INPUT /usr/local/texlive/2022/texmf-dist/fonts/type1/public/amsfonts/cm/cmex10.pfb
INPUT /usr/local/texlive/2022/texmf-dist/fonts/type1/public/amsfonts/cm/cmmi10.pfb
INPUT /usr/local/texlive/2022/texmf-dist/fonts/type1/public/amsfonts/cm/cmmi7.pfb
INPUT /usr/local/texlive/2022/texmf-dist/fonts/type1/public/amsfonts/cm/cmr10.pfb
INPUT /usr/local/texlive/2022/texmf-dist/fonts/type1/public/amsfonts/cm/cmr5.pfb
INPUT /usr/local/texlive/2022/texmf-dist/fonts/type1/public/amsfonts/cm/cmr7.pfb
INPUT /usr/local/texlive/2022/texmf-dist/fonts/type1/public/amsfonts/cm/cmr8.pfb
INPUT /usr/local/texlive/2022/texmf-dist/fonts/type1/public/amsfonts/cm/cmsy10.pfb
INPUT /usr/local/texlive/2022/texmf-dist/fonts/type1/public/amsfonts/cm/cmsy5.pfb
INPUT /usr/local/texlive/2022/texmf-dist/fonts/type1/public/amsfonts/cm/cmsy7.pfb
INPUT /usr/local/texlive/2022/texmf-dist/fonts/type1/public/amsfonts/cm/cmti10.pfb
INPUT /usr/local/texlive/2022/texmf-dist/fonts/type1/public/amsfonts/cm/cmti8.pfb
INPUT /usr/local/texlive/2022/texmf-dist/fonts/type1/public/amsfonts/cm/cmtt8.pfb
INPUT /usr/local/texlive/2022/texmf-dist/fonts/type1/public/amsfonts/symbols/msam10.pfb
INPUT /usr/local/texlive/2022/texmf-dist/fonts/type1/public/amsfonts/symbols/msbm10.pfb
+22 -12
View File
@@ -1,4 +1,4 @@
This is pdfTeX, Version 3.141592653-2.6-1.40.24 (TeX Live 2022) (preloaded format=pdflatex 2022.10.5) 12 APR 2026 22:19
This is pdfTeX, Version 3.141592653-2.6-1.40.24 (TeX Live 2022) (preloaded format=pdflatex 2022.10.5) 13 APR 2026 00:00
entering extended mode
restricted \write18 enabled.
file:line:error style messages enabled.
@@ -130,20 +130,30 @@ File: umsa.fd 2013/01/14 v3.01 AMS symbols A
LaTeX Font Info: Trying to load font information for U+msb on input line 52.
(/usr/local/texlive/2022/texmf-dist/tex/latex/amsfonts/umsb.fd
File: umsb.fd 2013/01/14 v3.01 AMS symbols B
) [1{/usr/local/texlive/2022/texmf-var/fonts/map/pdftex/updmap/pdftex.map}] (./paper.aux) )
) [1{/usr/local/texlive/2022/texmf-var/fonts/map/pdftex/updmap/pdftex.map}] [2] [3]
Overfull \hbox (2.17857pt too wide) in paragraph at lines 247--248
\OT1/cmr/bx/n/10 Lemma 3.2. \OT1/cmr/m/it/10 For each $\OML/cmm/m/it/10 G[] \OMS/cmsy/m/n/10 2 M$\OT1/cmr/m/it/10 , the ex-ten-sions of $\OT1/cmr/m/n/10 ^^H[](\OML/cmm/m/it/10 G[]\OT1/cmr/m/n/10 )$ \OT1/cmr/m/it/10 lie in $\OT1/cmr/m/n/10 ^^H[]$\OT1/cmr/m/it/10 , i.e., $[] \OMS/cmsy/m/n/10 ^^R
[]
Overfull \hbox (18.04422pt too wide) detected at line 257
[]\OT1/cmr/m/n/10 (\OML/cmm/m/it/10 N\OT1/cmr/m/n/10 (\OML/cmm/m/it/10 v[]\OT1/cmr/m/n/10 )) = [](\OMS/cmsy/m/n/10 f\OML/cmm/m/it/10 a[]; a[]\OMS/cmsy/m/n/10 g [ \OT1/cmr/m/n/10 (\OML/cmm/m/it/10 N\OT1/cmr/m/n/10 (\OML/cmm/m/it/10 v[]\OT1/cmr/m/n/10 ) \OMS/cmsy/m/n/10 n f\OML/cmm/m/it/10 a[]; a[]\OMS/cmsy/m/n/10 g\OT1/cmr/m/n/10 )) = \OMS/cmsy/m/n/10 f\OML/cmm/m/it/10 \OT1/cmr/m/n/10 (\OML/cmm/m/it/10 a[]\OT1/cmr/m/n/10 )\OMS/cmsy/m/n/10 g [ \OML/cmm/m/it/10 \OT1/cmr/m/n/10 (\OML/cmm/m/it/10 N\OT1/cmr/m/n/10 (\OML/cmm/m/it/10 v[]\OT1/cmr/m/n/10 ) \OMS/cmsy/m/n/10 n f\OML/cmm/m/it/10 a[]; a[]\OMS/cmsy/m/n/10 g\OT1/cmr/m/n/10 ) = \OML/cmm/m/it/10 \OT1/cmr/m/n/10 (\OML/cmm/m/it/10 N[]\OT1/cmr/m/n/10 (\OML/cmm/m/it/10 v[]\OT1/cmr/m/n/10 ))\OML/cmm/m/it/10 :
[]
[4] (./paper.aux) )
Here is how much of TeX's memory you used:
1710 strings out of 478268
23958 string characters out of 5846347
316202 words of memory out of 5000000
19795 multiletter control sequences out of 15000+600000
474133 words of font info for 47 fonts, out of 8000000 for 9000
1719 strings out of 478268
24065 string characters out of 5846347
330202 words of memory out of 5000000
19803 multiletter control sequences out of 15000+600000
475834 words of font info for 54 fonts, out of 8000000 for 9000
1302 hyphenation exceptions out of 8191
69i,5n,76p,280b,204s stack positions out of 10000i,1000n,20000p,200000b,200000s
</usr/local/texlive/2022/texmf-dist/fonts/type1/public/amsfonts/cm/cmbx10.pfb></usr/local/texlive/2022/texmf-dist/fonts/type1/public/amsfonts/cm/cmcsc10.pfb></usr/local/texlive/2022/texmf-dist/fonts/type1/public/amsfonts/cm/cmr7.pfb></usr/local/texlive/2022/texmf-dist/fonts/type1/public/amsfonts/cm/cmr8.pfb></usr/local/texlive/2022/texmf-dist/fonts/type1/public/amsfonts/cm/cmti8.pfb></usr/local/texlive/2022/texmf-dist/fonts/type1/public/amsfonts/cm/cmtt8.pfb>
Output written on paper.pdf (1 page, 64345 bytes).
69i,9n,76p,727b,280s stack positions out of 10000i,1000n,20000p,200000b,200000s
</usr/local/texlive/2022/texmf-dist/fonts/type1/public/amsfonts/cm/cmbx10.pfb></usr/local/texlive/2022/texmf-dist/fonts/type1/public/amsfonts/cm/cmcsc10.pfb></usr/local/texlive/2022/texmf-dist/fonts/type1/public/amsfonts/cm/cmex10.pfb></usr/local/texlive/2022/texmf-dist/fonts/type1/public/amsfonts/cm/cmmi10.pfb></usr/local/texlive/2022/texmf-dist/fonts/type1/public/amsfonts/cm/cmmi7.pfb></usr/local/texlive/2022/texmf-dist/fonts/type1/public/amsfonts/cm/cmr10.pfb></usr/local/texlive/2022/texmf-dist/fonts/type1/public/amsfonts/cm/cmr5.pfb></usr/local/texlive/2022/texmf-dist/fonts/type1/public/amsfonts/cm/cmr7.pfb></usr/local/texlive/2022/texmf-dist/fonts/type1/public/amsfonts/cm/cmr8.pfb></usr/local/texlive/2022/texmf-dist/fonts/type1/public/amsfonts/cm/cmsy10.pfb></usr/local/texlive/2022/texmf-dist/fonts/type1/public/amsfonts/cm/cmsy5.pfb></usr/local/texlive/2022/texmf-dist/fonts/type1/public/amsfonts/cm/cmsy7.pfb></usr/local/texlive/2022/texmf-dist/fonts/type1/public/amsfonts/cm/cmti10.pfb></usr/local/texlive/2022/texmf-dist/fonts/type1/public/amsfonts/cm/cmti8.pfb></usr/local/texlive/2022/texmf-dist/fonts/type1/public/amsfonts/cm/cmtt8.pfb></usr/local/texlive/2022/texmf-dist/fonts/type1/public/amsfonts/symbols/msam10.pfb></usr/local/texlive/2022/texmf-dist/fonts/type1/public/amsfonts/symbols/msbm10.pfb>
Output written on paper.pdf (4 pages, 213600 bytes).
PDF statistics:
38 PDF objects out of 1000 (max. 8388607)
22 compressed objects within 1 object stream
102 PDF objects out of 1000 (max. 8388607)
61 compressed objects within 1 object stream
0 named destinations out of 1000 (max. 500000)
1 words of extra memory for PDF output out of 10000 (max. 10000000)
BIN
View File
Binary file not shown.
BIN
View File
Binary file not shown.
+176
View File
@@ -82,6 +82,182 @@
\maketitle
\section{Kempe's Proof (Valid Portion)}
\subsection{Setup}
Kempe's strategy, published in 1879, follows a \emph{minimal counterexample} argument. Suppose, for contradiction, that there exists a planar graph requiring 5 colors. Among all such graphs, let $G$ be one with the fewest vertices. Then every planar graph with fewer vertices than $G$ is 4-colorable, but $G$ itself is not.
\subsection{Every Planar Graph Has a Vertex of Degree at Most 5}
\begin{lemma}
Every planar graph has at least one vertex of degree $\leq 5$.
\end{lemma}
\begin{proof}
Let $G$ be a connected planar graph with $V$ vertices, $E$ edges, and $F$ faces. By Euler's formula,
\[
V - E + F = 2.
\]
Since every face is bounded by at least 3 edges and each edge borders at most 2 faces, we have $2E \geq 3F$, hence $F \leq \frac{2E}{3}$. Substituting into Euler's formula:
\[
V - E + \frac{2E}{3} \geq 2 \implies E \leq 3V - 6.
\]
If every vertex had degree $\geq 6$, then $2E \geq 6V$, so $E \geq 3V$, contradicting $E \leq 3V - 6$. Therefore at least one vertex has degree $\leq 5$.
\end{proof}
Since $G$ is a minimal counterexample, it must contain a vertex $v$ of degree at most 5. Kempe argued by cases on the degree of $v$.
\subsection{Cases of Degree at Most 3}
Suppose $v$ has degree $\leq 3$. Remove $v$ from $G$ to obtain the graph $G - v$. Since $G - v$ has fewer vertices than $G$, it is 4-colorable by minimality. Fix such a 4-coloring. Now reinsert $v$: its at most 3 neighbors occupy at most 3 of the 4 colors, so at least one color remains available for $v$. This yields a valid 4-coloring of $G$, a contradiction.
\subsection{Case of Degree 4}
Suppose $v$ has degree exactly 4 with neighbors $a$, $b$, $c$, $d$ appearing in cyclic order around $v$ in the planar embedding. Remove $v$ and 4-color $G - v$ by minimality. If the four neighbors do not all receive distinct colors, then at least one color is unused among them, and we may assign that color to $v$, giving a contradiction.
So assume $a$, $b$, $c$, $d$ receive all four distinct colors; call them $1$, $2$, $3$, $4$ respectively. Define a \emph{Kempe chain} to be a maximal connected subgraph whose vertices are colored with exactly two specified colors.
Consider the Kempe chain $K_{13}$ containing $a$ (using colors 1 and 3).
\begin{itemize}
\item \textbf{Case 1}: $c$ is not in $K_{13}$. Swap colors 1 and 3 throughout $K_{13}$. This is still a valid coloring of $G - v$, and now $a$ receives color 3, so color 1 is free for $v$.
\item \textbf{Case 2}: $c$ is in $K_{13}$. Then there is a path of alternating colors 1 and 3 from $a$ to $c$ in the planar embedding. Because $a$ and $c$ alternate around $v$ with $b$ and $d$, this path separates $b$ from $d$ in the plane. Therefore $b$ and $d$ lie in different Kempe chains for colors 2 and 4. Swap colors 2 and 4 in the chain containing $b$; now $b$ receives color 4, freeing color 2 for $v$.
\end{itemize}
In both cases we obtain a valid 4-coloring of $G$, a contradiction.
\section{Resolution of Degree 5 Case}
\subsection{At Least 12 Vertices of Degree 5}
Since we have already handled every vertex of degree $\leq 4$, we may assume without loss of generality that the minimal counterexample $G$ has minimum degree 5. We now show that $G$ must contain at least 12 vertices of degree exactly 5.
\begin{lemma}
If $G$ is a planar graph with minimum degree 5, then $G$ contains at least 12 vertices of degree exactly 5.
\end{lemma}
\begin{proof}
For each $k \geq 5$, let $n_k$ denote the number of vertices of degree exactly $k$ in $G$. Since every vertex has degree $\geq 5$,
\[
V = \sum_{k \geq 5} n_k, \qquad 2E = \sum_{k \geq 5} k\, n_k.
\]
Using $E \leq 3V - 6$, we obtain $2E \leq 6V - 12$, so
\[
\sum_{k \geq 5} k\, n_k \leq 6\sum_{k \geq 5} n_k - 12.
\]
Moving all terms to the right-hand side gives
\[
12 \leq 6\sum_{k \geq 5} n_k - \sum_{k \geq 5} k\, n_k = \sum_{k \geq 5} (6 - k)\, n_k.
\]
We now expand this sum by separating the $k = 5$, $k = 6$, and $k \geq 7$ terms:
\[
\sum_{k \geq 5}(6-k)\,n_k
= \underbrace{(6-5)\,n_5}_{=\,n_5}
+ \underbrace{(6-6)\,n_6}_{=\,0}
+ \sum_{k \geq 7}(6-k)\,n_k
= n_5 - \sum_{k \geq 7}(k-6)\,n_k.
\]
Therefore $12 \leq n_5 - \sum_{k \geq 7}(k-6)\,n_k$, which rearranges to
\[
n_5 \geq 12 + \sum_{k \geq 7}(k-6)\,n_k.
\]
Since $k - 6 \geq 1 > 0$ and $n_k \geq 0$ for all $k \geq 7$, each term in the sum is non-negative, so $\sum_{k \geq 7}(k-6)\,n_k \geq 0$ and thus $n_5 \geq 12$.
\end{proof}
\subsection{Two Non-Adjacent Vertices of Degree 5}
\begin{lemma}
If $G$ is a planar graph with minimum degree 5, then $G$ contains two non-adjacent vertices of degree exactly 5.
\end{lemma}
\begin{proof}
By the previous lemma, $G$ contains at least 12 vertices of degree exactly 5. Let $S$ denote the set of all degree-5 vertices, so $|S| \geq 12$. Suppose for contradiction that every two vertices in $S$ are adjacent, i.e., $S$ induces a clique in $G$. Then every vertex $v \in S$ is adjacent to all other $|S| - 1 \geq 11$ vertices of $S$. But $\deg(v) = 5$, so $v$ has at most 5 neighbors in total. Since $11 > 5$, this is a contradiction. Therefore $S$ does not form a clique, and there exist two vertices $v_1, v_2 \in S$ that are non-adjacent.
\end{proof}
\subsection{The Reduced Subgraph $G'$}
By the previous lemma, we may fix two non-adjacent vertices $v_0, v_1 \in G$ each of degree 5. Define
\[
G' = G - \{v_0, v_1\},
\]
as the subgraph of $G$ obtained by deleting $v_0$ and $v_1$ together with all edges incident to either vertex. Since $G'$ has strictly fewer vertices than $G$, the minimality of $G$ guarantees that $G'$ admits a proper 4-coloring $\phi : V(G') \to \{1,2,3,4\}$. Because $v_0$ and $v_1$ are non-adjacent in $G$, neither is a neighbor of the other, so each retains all 5 of its neighbors in $G'$. Let $N(v_i)$ denote the set of neighbors of $v_i$ in $G$; then $N(v_0)$ and $N(v_1)$ are each sets of 5 vertices, all of which lie in $G'$ and are assigned colors by $\phi$. Note also that $N(v_0)$ and $N(v_1)$ may overlap. Let $\Phi$ be the set of all possible 4-colorings of $G'$.
\subsection{Not All Colorings in $\Phi$ Saturate Both Neighborhoods}
\begin{lemma}
It is not possible that every $\phi \in \Phi$ satisfies both $|\phi(N(v_0))| = 4$ and $|\phi(N(v_1))| = 4$.
\end{lemma}
\begin{proof}
We show the stronger fact that there exists $\phi \in \Phi$ with $|\phi(N(v_0))| \leq 3$.
Since $v_1$ is a single vertex, $G - \{v_1\}$ is a planar graph on $V - 1$ vertices. Because $V - 1 < V$ and $G$ is a minimal counterexample, $G - \{v_1\}$ is 4-colorable. Fix a proper 4-coloring $\psi$ of $G - \{v_1\}$. This coloring assigns a color to every vertex of $G'$ and also to $v_0$.
Let $\phi = \psi|_{V(G')}$ be the restriction of $\psi$ to $G'$. Since $\psi$ is a proper coloring of $G - \{v_1\} \supseteq G'$, the restriction $\phi$ is a proper 4-coloring of $G'$, so $\phi \in \Phi$.
Because $\psi$ is a proper coloring of $G - \{v_1\}$ and $v_0 \in V(G - \{v_1\})$, the color $\psi(v_0)$ differs from the color of every neighbor of $v_0$. In particular, $\psi(v_0) \notin \phi(N(v_0))$. Since $\psi(v_0) \in \{1,2,3,4\}$ and $\psi(v_0)$ does not appear in $\phi(N(v_0))$, it follows that $|\phi(N(v_0))| \leq 3$. Therefore not every coloring in $\Phi$ uses all 4 colors on $N(v_0)$, and in particular it is impossible that every $\phi \in \Phi$ saturates both $N(v_0)$ and $N(v_1)$ with all 4 colors.
\end{proof}
\section{Merged Subgraphs of $G'$}
Let $N(v_0) = \{a_0, a_1, a_2, a_3, a_4\}$ be the five neighbors of $v_0$ in $G'$. For each pair of non-adjacent vertices $a_i, a_j \in N(v_0)$ (i.e., $\{a_i, a_j\} \notin E(G')$), define the graph $G'_{ij}$ to be the result of identifying $a_i$ and $a_j$ in $G'$: formally, $G'_{ij}$ is obtained from $G'$ by removing $a_i$ and $a_j$ and adding a new vertex $a_{ij}$ adjacent to every vertex in $N_{G'}(a_i) \cup N_{G'}(a_j)$. Define the set of all such merged subgraphs by
\[
\mathcal{M} = \bigl\{\, G'_{ij} : a_i, a_j \in N(v_0),\ \{a_i, a_j\} \notin E(G') \,\bigr\}.
\]
\subsection{Colorings of Merged Subgraphs Extend to $G'$}
For each $G'_{ij} \in \mathcal{M}$, let $\Phi(G'_{ij})$ denote the set of proper 4-colorings of $G'_{ij}$. Each such coloring can be extended to a coloring of $G'$ by assigning the color of the merged vertex $a_{ij}$ back to both $a_i$ and $a_j$. Formally, for $\psi \in \Phi(G'_{ij})$, define $\widetilde{\psi} : V(G') \to \{1,2,3,4\}$ by
\[
\widetilde{\psi}(v) = \begin{cases} \psi(a_{ij}) & \text{if } v = a_i \text{ or } v = a_j, \\ \psi(v) & \text{otherwise.} \end{cases}
\]
Let $\widetilde{\Phi}_{ij} = \{\,\widetilde{\psi} : \psi \in \Phi(G'_{ij})\,\}$ denote the set of all such extensions.
\begin{lemma}
For each $G'_{ij} \in \mathcal{M}$, we have $\widetilde{\Phi}_{ij} \subseteq \Phi$.
\end{lemma}
\begin{proof}
Let $\psi \in \Phi(G'_{ij})$ and let $\widetilde{\psi}$ be its extension to $G'$. We verify that $\widetilde{\psi}$ is a proper coloring of $G'$ by checking every edge $\{u, w\} \in E(G')$.
\textbf{Case 1: neither $u$ nor $w$ is $a_i$ or $a_j$.} Then $\{u, w\}$ is also an edge of $G'_{ij}$, and $\widetilde{\psi}(u) = \psi(u) \neq \psi(w) = \widetilde{\psi}(w)$.
\textbf{Case 2: $u \in \{a_i, a_j\}$ and $w \notin \{a_i, a_j\}$ (or vice versa).} Then $w \in N_{G'}(a_i) \cup N_{G'}(a_j)$, so $w$ is adjacent to $a_{ij}$ in $G'_{ij}$. Since $\psi$ is proper, $\psi(w) \neq \psi(a_{ij}) = \widetilde{\psi}(u)$.
\textbf{Case 3: $u = a_i$ and $w = a_j$.} This case cannot occur, since $a_i$ and $a_j$ are non-adjacent in $G'$ by the definition of $\mathcal{M}$.
In all cases the endpoints of every edge receive distinct colors, so $\widetilde{\psi} \in \Phi$.
\end{proof}
\subsection{4-Saturating Merged Colorings Extend to 4-Saturating Colorings of $G'$}
For each $G'_{ij} \in \mathcal{M}$, the vertices of $G'_{ij}$ that would be adjacent to $v_0$ if $v_0$ were reinserted are exactly $\{a_{ij}\} \cup (N(v_0) \setminus \{a_i, a_j\})$; call this set $N_{ij}(v_0)$. Define
\[
\Phi_4 = \{\, \phi \in \Phi : |\phi(N(v_0))| = 4 \,\}
\]
to be the set of colorings of $G'$ that use all 4 colors on $N(v_0)$, and for each $G'_{ij} \in \mathcal{M}$ define
\[
\Phi_4(G'_{ij}) = \{\, \psi \in \Phi(G'_{ij}) : |\psi(N_{ij}(v_0))| = 4 \,\}
\]
to be the colorings of $G'_{ij}$ that use all 4 colors on the effective neighborhood of $v_0$.
\begin{lemma}
For each $G'_{ij} \in \mathcal{M}$, the extensions of $\Phi_4(G'_{ij})$ lie in $\Phi_4$, i.e., $\widetilde{\Phi_4(G'_{ij})} \subseteq \Phi_4$.
\end{lemma}
\begin{proof}
Let $\psi \in \Phi_4(G'_{ij})$, so $|\psi(N_{ij}(v_0))| = 4$. By definition of the extension,
\[
\widetilde{\psi}(N(v_0))
= \widetilde{\psi}(\{a_i, a_j\} \cup (N(v_0) \setminus \{a_i, a_j\}))
= \{\psi(a_{ij})\} \cup \psi(N(v_0) \setminus \{a_i, a_j\})
= \psi(N_{ij}(v_0)).
\]
The first equality expands $N(v_0)$; the second uses $\widetilde{\psi}(a_i) = \widetilde{\psi}(a_j) = \psi(a_{ij})$ and $\widetilde{\psi}(u) = \psi(u)$ for $u \notin \{a_i, a_j\}$; the third uses $N_{ij}(v_0) = \{a_{ij}\} \cup (N(v_0) \setminus \{a_i,a_j\})$. Therefore $|\widetilde{\psi}(N(v_0))| = |\psi(N_{ij}(v_0))| = 4$. Since also $\widetilde{\psi} \in \Phi$ by the previous lemma, we conclude $\widetilde{\psi} \in \Phi_4$.
\end{proof}
\end{document}
%-----------------------------------------------------------------------