coloring_nested_tire_graphs: add Birkhoff-Heesch reducibility note and dictionary to fiber view

Summarises classical reducibility theory (Birkhoff 1913, Heesch
discharging, Appel-Haken, RSST) in modern notation, then maps it
onto the spoke-fiber decomposition: ring colorings ↔ spoke configs,
good/bad colorings ↔ realisable/unrealisable σ, D-reducibility ↔
chain-pigeonhole conductivity. Honest assessment: framework gives
vocabulary and a Sage-checkable template for small tires, but does
not give a uniform argument across tire sizes.

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

papers/coloring_nested_tire_graphs/notes/birkhoff_heesch_reducibility.aux

@@ -0,0 +1,13 @@
+\relax 
+\citation{thomas-update}
+\citation{thomas-update}
+\citation{bauerfeld-pds}
+\citation{tutte-chromial}
+\bibcite{birkhoff}{1}
+\bibcite{heesch}{2}
+\bibcite{appel-haken}{3}
+\bibcite{rsst}{4}
+\bibcite{thomas-update}{5}
+\bibcite{tutte-chromial}{6}
+\bibcite{bauerfeld-pds}{7}
+\gdef \@abspage@last{7}

papers/coloring_nested_tire_graphs/notes/birkhoff_heesch_reducibility.log

@@ -0,0 +1,312 @@
+This is pdfTeX, Version 3.141592653-2.6-1.40.24 (TeX Live 2022) (preloaded format=pdflatex 2022.10.5)  26 MAY 2026 01:08
+entering extended mode
+ restricted \write18 enabled.
+ %&-line parsing enabled.
+**birkhoff_heesch_reducibility.tex
+(./birkhoff_heesch_reducibility.tex
+LaTeX2e <2021-11-15> patch level 1
+L3 programming layer <2022-02-24>
+(/usr/local/texlive/2022/texmf-dist/tex/latex/base/article.cls
+Document Class: article 2021/10/04 v1.4n Standard LaTeX document class
+(/usr/local/texlive/2022/texmf-dist/tex/latex/base/size11.clo
+File: size11.clo 2021/10/04 v1.4n Standard LaTeX file (size option)
+)
+\c@part=\count185
+\c@section=\count186
+\c@subsection=\count187
+\c@subsubsection=\count188
+\c@paragraph=\count189
+\c@subparagraph=\count190
+\c@figure=\count191
+\c@table=\count192
+\abovecaptionskip=\skip47
+\belowcaptionskip=\skip48
+\bibindent=\dimen138
+)
+(/usr/local/texlive/2022/texmf-dist/tex/latex/amsmath/amsmath.sty
+Package: amsmath 2021/10/15 v2.17l AMS math features
+\@mathmargin=\skip49
+
+For additional information on amsmath, use the `?' option.
+(/usr/local/texlive/2022/texmf-dist/tex/latex/amsmath/amstext.sty
+Package: amstext 2021/08/26 v2.01 AMS text
+
+(/usr/local/texlive/2022/texmf-dist/tex/latex/amsmath/amsgen.sty
+File: amsgen.sty 1999/11/30 v2.0 generic functions
+\@emptytoks=\toks16
+\ex@=\dimen139
+))
+(/usr/local/texlive/2022/texmf-dist/tex/latex/amsmath/amsbsy.sty
+Package: amsbsy 1999/11/29 v1.2d Bold Symbols
+\pmbraise@=\dimen140
+)
+(/usr/local/texlive/2022/texmf-dist/tex/latex/amsmath/amsopn.sty
+Package: amsopn 2021/08/26 v2.02 operator names
+)
+\inf@bad=\count193
+LaTeX Info: Redefining \frac on input line 234.
+\uproot@=\count194
+\leftroot@=\count195
+LaTeX Info: Redefining \overline on input line 399.
+\classnum@=\count196
+\DOTSCASE@=\count197
+LaTeX Info: Redefining \ldots on input line 496.
+LaTeX Info: Redefining \dots on input line 499.
+LaTeX Info: Redefining \cdots on input line 620.
+\Mathstrutbox@=\box50
+\strutbox@=\box51
+\big@size=\dimen141
+LaTeX Font Info:    Redeclaring font encoding OML on input line 743.
+LaTeX Font Info:    Redeclaring font encoding OMS on input line 744.
+\macc@depth=\count198
+\c@MaxMatrixCols=\count199
+\dotsspace@=\muskip16
+\c@parentequation=\count266
+\dspbrk@lvl=\count267
+\tag@help=\toks17
+\row@=\count268
+\column@=\count269
+\maxfields@=\count270
+\andhelp@=\toks18
+\eqnshift@=\dimen142
+\alignsep@=\dimen143
+\tagshift@=\dimen144
+\tagwidth@=\dimen145
+\totwidth@=\dimen146
+\lineht@=\dimen147
+\@envbody=\toks19
+\multlinegap=\skip50
+\multlinetaggap=\skip51
+\mathdisplay@stack=\toks20
+LaTeX Info: Redefining \[ on input line 2938.
+LaTeX Info: Redefining \] on input line 2939.
+)
+(/usr/local/texlive/2022/texmf-dist/tex/latex/amsfonts/amssymb.sty
+Package: amssymb 2013/01/14 v3.01 AMS font symbols
+
+(/usr/local/texlive/2022/texmf-dist/tex/latex/amsfonts/amsfonts.sty
+Package: amsfonts 2013/01/14 v3.01 Basic AMSFonts support
+\symAMSa=\mathgroup4
+\symAMSb=\mathgroup5
+LaTeX Font Info:    Redeclaring math symbol \hbar on input line 98.
+LaTeX Font Info:    Overwriting math alphabet `\mathfrak' in version `bold'
+(Font)                  U/euf/m/n --> U/euf/b/n on input line 106.
+))
+(/usr/local/texlive/2022/texmf-dist/tex/latex/amscls/amsthm.sty
+Package: amsthm 2020/05/29 v2.20.6
+\thm@style=\toks21
+\thm@bodyfont=\toks22
+\thm@headfont=\toks23
+\thm@notefont=\toks24
+\thm@headpunct=\toks25
+\thm@preskip=\skip52
+\thm@postskip=\skip53
+\thm@headsep=\skip54
+\dth@everypar=\toks26
+)
+(/usr/local/texlive/2022/texmf-dist/tex/latex/graphics/graphicx.sty
+Package: graphicx 2021/09/16 v1.2d Enhanced LaTeX Graphics (DPC,SPQR)
+
+(/usr/local/texlive/2022/texmf-dist/tex/latex/graphics/keyval.sty
+Package: keyval 2014/10/28 v1.15 key=value parser (DPC)
+\KV@toks@=\toks27
+)
+(/usr/local/texlive/2022/texmf-dist/tex/latex/graphics/graphics.sty
+Package: graphics 2021/03/04 v1.4d Standard LaTeX Graphics (DPC,SPQR)
+
+(/usr/local/texlive/2022/texmf-dist/tex/latex/graphics/trig.sty
+Package: trig 2021/08/11 v1.11 sin cos tan (DPC)
+)
+(/usr/local/texlive/2022/texmf-dist/tex/latex/graphics-cfg/graphics.cfg
+File: graphics.cfg 2016/06/04 v1.11 sample graphics configuration
+)
+Package graphics Info: Driver file: pdftex.def on input line 107.
+
+(/usr/local/texlive/2022/texmf-dist/tex/latex/graphics-def/pdftex.def
+File: pdftex.def 2020/10/05 v1.2a Graphics/color driver for pdftex
+))
+\Gin@req@height=\dimen148
+\Gin@req@width=\dimen149
+)
+(/usr/local/texlive/2022/texmf-dist/tex/latex/geometry/geometry.sty
+Package: geometry 2020/01/02 v5.9 Page Geometry
+
+(/usr/local/texlive/2022/texmf-dist/tex/generic/iftex/ifvtex.sty
+Package: ifvtex 2019/10/25 v1.7 ifvtex legacy package. Use iftex instead.
+
+(/usr/local/texlive/2022/texmf-dist/tex/generic/iftex/iftex.sty
+Package: iftex 2022/02/03 v1.0f TeX engine tests
+))
+\Gm@cnth=\count271
+\Gm@cntv=\count272
+\c@Gm@tempcnt=\count273
+\Gm@bindingoffset=\dimen150
+\Gm@wd@mp=\dimen151
+\Gm@odd@mp=\dimen152
+\Gm@even@mp=\dimen153
+\Gm@layoutwidth=\dimen154
+\Gm@layoutheight=\dimen155
+\Gm@layouthoffset=\dimen156
+\Gm@layoutvoffset=\dimen157
+\Gm@dimlist=\toks28
+)
+(/usr/local/texlive/2022/texmf-dist/tex/latex/caption/caption.sty
+Package: caption 2022/03/01 v3.6b Customizing captions (AR)
+
+(/usr/local/texlive/2022/texmf-dist/tex/latex/caption/caption3.sty
+Package: caption3 2022/03/17 v2.3b caption3 kernel (AR)
+\caption@tempdima=\dimen158
+\captionmargin=\dimen159
+\caption@leftmargin=\dimen160
+\caption@rightmargin=\dimen161
+\caption@width=\dimen162
+\caption@indent=\dimen163
+\caption@parindent=\dimen164
+\caption@hangindent=\dimen165
+Package caption Info: Standard document class detected.
+)
+\c@caption@flags=\count274
+\c@continuedfloat=\count275
+)
+(/usr/local/texlive/2022/texmf-dist/tex/latex/tools/array.sty
+Package: array 2021/10/04 v2.5f Tabular extension package (FMi)
+\col@sep=\dimen166
+\ar@mcellbox=\box52
+\extrarowheight=\dimen167
+\NC@list=\toks29
+\extratabsurround=\skip55
+\backup@length=\skip56
+\ar@cellbox=\box53
+)
+(/usr/local/texlive/2022/texmf-dist/tex/latex/l3backend/l3backend-pdftex.def
+File: l3backend-pdftex.def 2022-02-07 L3 backend support: PDF output (pdfTeX)
+\l__color_backend_stack_int=\count276
+\l__pdf_internal_box=\box54
+)
+(./birkhoff_heesch_reducibility.aux)
+\openout1 = `birkhoff_heesch_reducibility.aux'.
+
+LaTeX Font Info:    Checking defaults for OML/cmm/m/it on input line 19.
+LaTeX Font Info:    ... okay on input line 19.
+LaTeX Font Info:    Checking defaults for OMS/cmsy/m/n on input line 19.
+LaTeX Font Info:    ... okay on input line 19.
+LaTeX Font Info:    Checking defaults for OT1/cmr/m/n on input line 19.
+LaTeX Font Info:    ... okay on input line 19.
+LaTeX Font Info:    Checking defaults for T1/cmr/m/n on input line 19.
+LaTeX Font Info:    ... okay on input line 19.
+LaTeX Font Info:    Checking defaults for TS1/cmr/m/n on input line 19.
+LaTeX Font Info:    ... okay on input line 19.
+LaTeX Font Info:    Checking defaults for OMX/cmex/m/n on input line 19.
+LaTeX Font Info:    ... okay on input line 19.
+LaTeX Font Info:    Checking defaults for U/cmr/m/n on input line 19.
+LaTeX Font Info:    ... okay on input line 19.
+
+(/usr/local/texlive/2022/texmf-dist/tex/context/base/mkii/supp-pdf.mkii
+[Loading MPS to PDF converter (version 2006.09.02).]
+\scratchcounter=\count277
+\scratchdimen=\dimen168
+\scratchbox=\box55
+\nofMPsegments=\count278
+\nofMParguments=\count279
+\everyMPshowfont=\toks30
+\MPscratchCnt=\count280
+\MPscratchDim=\dimen169
+\MPnumerator=\count281
+\makeMPintoPDFobject=\count282
+\everyMPtoPDFconversion=\toks31
+) (/usr/local/texlive/2022/texmf-dist/tex/latex/epstopdf-pkg/epstopdf-base.sty
+Package: epstopdf-base 2020-01-24 v2.11 Base part for package epstopdf
+Package epstopdf-base Info: Redefining graphics rule for `.eps' on input line 4
+85.
+
+(/usr/local/texlive/2022/texmf-dist/tex/latex/latexconfig/epstopdf-sys.cfg
+File: epstopdf-sys.cfg 2010/07/13 v1.3 Configuration of (r)epstopdf for TeX Liv
+e
+))
+*geometry* driver: auto-detecting
+*geometry* detected driver: pdftex
+*geometry* verbose mode - [ preamble ] result:
+* driver: pdftex
+* paper: <default>
+* layout: <same size as paper>
+* layoutoffset:(h,v)=(0.0pt,0.0pt)
+* modes: 
+* h-part:(L,W,R)=(72.26999pt, 469.75502pt, 72.26999pt)
+* v-part:(T,H,B)=(72.26999pt, 650.43001pt, 72.26999pt)
+* \paperwidth=614.295pt
+* \paperheight=794.96999pt
+* \textwidth=469.75502pt
+* \textheight=650.43001pt
+* \oddsidemargin=0.0pt
+* \evensidemargin=0.0pt
+* \topmargin=-37.0pt
+* \headheight=12.0pt
+* \headsep=25.0pt
+* \topskip=11.0pt
+* \footskip=30.0pt
+* \marginparwidth=59.0pt
+* \marginparsep=10.0pt
+* \columnsep=10.0pt
+* \skip\footins=10.0pt plus 4.0pt minus 2.0pt
+* \hoffset=0.0pt
+* \voffset=0.0pt
+* \mag=1000
+* \@twocolumnfalse
+* \@twosidefalse
+* \@mparswitchfalse
+* \@reversemarginfalse
+* (1in=72.27pt=25.4mm, 1cm=28.453pt)
+
+Package caption Info: Begin \AtBeginDocument code.
+Package caption Info: End \AtBeginDocument code.
+LaTeX Font Info:    Trying to load font information for U+msa on input line 20.
+
+(/usr/local/texlive/2022/texmf-dist/tex/latex/amsfonts/umsa.fd
+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 20.
+
+
+(/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}] [2] [3]
+ [4] [5]
+[6] [7] (./birkhoff_heesch_reducibility.aux) ) 
+Here is how much of TeX's memory you used:
+ 4568 strings out of 478268
+ 73987 string characters out of 5846347
+ 376623 words of memory out of 5000000
+ 22749 multiletter control sequences out of 15000+600000
+ 479245 words of font info for 64 fonts, out of 8000000 for 9000
+ 1141 hyphenation exceptions out of 8191
+ 55i,11n,63p,259b,221s stack positions out of 10000i,1000n,20000p,200000b,200000s
+{/usr/local/texlive/2022/texmf-di
+st/fonts/enc/dvips/cm-super/cm-super-ts1.enc}</usr/local/texlive/2022/texmf-dis
+t/fonts/type1/public/amsfonts/cm/cmbx10.pfb></usr/local/texlive/2022/texmf-dist
+/fonts/type1/public/amsfonts/cm/cmbx12.pfb></usr/local/texlive/2022/texmf-dist/
+fonts/type1/public/amsfonts/cm/cmbxti10.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/f
+onts/type1/public/amsfonts/cm/cmmi6.pfb></usr/local/texlive/2022/texmf-dist/fon
+ts/type1/public/amsfonts/cm/cmmi8.pfb></usr/local/texlive/2022/texmf-dist/fonts
+/type1/public/amsfonts/cm/cmr10.pfb></usr/local/texlive/2022/texmf-dist/fonts/t
+ype1/public/amsfonts/cm/cmr12.pfb></usr/local/texlive/2022/texmf-dist/fonts/typ
+e1/public/amsfonts/cm/cmr17.pfb></usr/local/texlive/2022/texmf-dist/fonts/type1
+/public/amsfonts/cm/cmr8.pfb></usr/local/texlive/2022/texmf-dist/fonts/type1/pu
+blic/amsfonts/cm/cmsy10.pfb></usr/local/texlive/2022/texmf-dist/fonts/type1/pub
+lic/amsfonts/cm/cmsy6.pfb></usr/local/texlive/2022/texmf-dist/fonts/type1/publi
+c/amsfonts/cm/cmsy8.pfb></usr/local/texlive/2022/texmf-dist/fonts/type1/public/
+amsfonts/cm/cmti10.pfb></usr/local/texlive/2022/texmf-dist/fonts/type1/public/a
+msfonts/cm/cmti8.pfb></usr/local/texlive/2022/texmf-dist/fonts/type1/public/ams
+fonts/cm/cmtt10.pfb></usr/local/texlive/2022/texmf-dist/fonts/type1/public/amsf
+onts/symbols/msbm10.pfb></usr/local/texlive/2022/texmf-dist/fonts/type1/public/
+cm-super/sfrm1095.pfb>
+Output written on birkhoff_heesch_reducibility.pdf (7 pages, 252748 bytes).
+PDF statistics:
+ 124 PDF objects out of 1000 (max. 8388607)
+ 76 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)
+

papers/coloring_nested_tire_graphs/notes/birkhoff_heesch_reducibility.tex

@@ -0,0 +1,466 @@
+\documentclass[11pt]{article}
+\usepackage{amsmath,amssymb,amsthm}
+\usepackage{graphicx}
+\usepackage{geometry}
+\usepackage{caption}
+\usepackage{array}
+\geometry{margin=1in}
+
+\title{Birkhoff--Heesch reducibility and the fiber view\\
+       \large A dictionary between classical 4CT reducibility theory
+       and our spoke-fiber decomposition}
+\author{}
+\date{}
+
+\newtheorem*{prop}{Proposition}
+\newtheorem*{thm}{Theorem}
+\newtheorem*{defn}{Definition}
+
+\begin{document}
+\maketitle
+
+\section*{Purpose}
+
+The conversation around the fiber decomposition note
+(\texttt{fiber\_decomposition.tex}) flagged that the technique of
+``split a coloring into a boundary configuration plus an
+extension-counting fiber'' is exactly the framework of classical
+reducibility theory for the Four-Color Theorem (4CT) --- developed by
+Birkhoff (1913), then Heesch, Bernhart, Allaire, Swart, Appel--Haken,
+and finally Robertson--Sanders--Seymour--Thomas (RSST, 1997).  This
+note (a) summarises the relevant pieces of that machinery in modern
+notation following Thomas's survey~\cite{thomas-update}, then (b)
+gives an explicit dictionary to our spoke-fiber language and an
+honest assessment of what carries over.
+
+\section*{Part I: classical reducibility, in modern notation}
+
+\subsection*{The 4CT and its Tait dual}
+
+\begin{thm}[4CT, vertex form]
+Every plane graph $G$ has a proper $4$-vertex-coloring.
+\end{thm}
+
+\begin{thm}[Tait 1880, edge form]
+Every cubic plane graph $H$ with no cut-edge has a proper $3$-edge-coloring.
+This is equivalent to the 4CT.
+\end{thm}
+
+The equivalence goes through planar duality: a $4$-coloring of a
+triangulation $G$, with colors $(0,0), (1,0), (0,1), (1,1)$ in
+$\mathbb{Z}_2 \times \mathbb{Z}_2$, induces a $3$-edge-coloring of the
+dual $G^*$ by assigning each dual edge the sum of the colors of the
+two regions it separates.  This is exactly the side our paper works
+on: a triangulation $G$ has a cubic dual $G' \subseteq G^*$
+(specifically: $G^*$ minus the unbounded face), and edge $3$-colorings
+of $G'$ \emph{are} (up to handling of the outer face) $4$-colorings of $G$.
+
+\subsection*{Birkhoff's minimum-counterexample setup (1913)}
+
+The reducibility programme assumes for contradiction that there is a
+\emph{minimum counterexample} to the 4CT --- a plane graph $T$ that is
+not $4$-colorable but every smaller plane graph is.  Birkhoff showed:
+
+\begin{thm}[Birkhoff 1913]
+Every minimum counterexample to the 4CT is an internally
+$6$-connected triangulation.
+\end{thm}
+
+(``Internally $6$-connected'' means: removing fewer than $5$ vertices
+keeps the graph connected, and removing any $5$ vertices leaves at
+most a single isolated vertex.)  All subsequent work assumes $T$ has
+this form.
+
+\subsection*{Configurations, rings, free completions}
+
+A \emph{configuration} captures a small local piece of $T$
+together with degree information.
+
+\begin{defn}[Configuration, Thomas~\cite{thomas-update}]
+A configuration is a pair $K = (H, \gamma)$ where $H$ is a
+near-triangulation (one face is designated as ``special'', and every
+other face is a triangle) and $\gamma : V(H) \to \mathbb{Z}_{\geq 5}$
+satisfies:
+\begin{enumerate}
+  \item[(i)]   for interior vertices $v$ (not on the special face),
+               $\gamma(v) = \deg_H(v)$;
+  \item[(ii)]  for boundary vertices $v$ (on the special face),
+               $\gamma(v) > \deg_H(v)$;
+  \item[(iii)] $\operatorname{ring-size}(K)
+                  := \sum_{v \text{ boundary}, H \setminus v \text{ connected}}
+                     (\gamma(v) - \deg_H(v) - 1) \geq 2$.
+\end{enumerate}
+$K$ \emph{appears} in a triangulation $T$ if $H$ is an induced subgraph
+of $T$, every non-special face of $H$ is a face of $T$, and $\gamma(v)$
+equals the degree of $v$ in $T$ for every $v \in V(H)$.
+\end{defn}
+
+\begin{defn}[Free completion]
+The \emph{free completion} of $K$ is the (essentially unique)
+plane graph $S$ obtained from $H$ by adding a single cycle $R$ --- the
+\emph{ring} of $K$ --- around the special face, plus the unique set of
+edges making $S$ a triangulation of the disk bounded by $R$ in which
+every vertex of $H$ has degree exactly $\gamma$.  $R$ has length equal
+to the ring-size of $K$.
+\end{defn}
+
+\subsection*{Color sets and reducibility}
+
+Let $\mathcal{K}(R)$ be the set of all proper $4$-colorings of the ring
+$R$ (often considered up to the $S_4$-action on colors, leaving roughly
+$|\mathcal{K}(R)|/24$ orbits).
+
+\begin{defn}[Good and bad colorings]
+A coloring $\varphi \in \mathcal{K}(R)$ is \emph{good} if it extends
+to a proper $4$-coloring of the free completion $S$, i.e.\ to all of
+$H \cup R$.  Otherwise it is \emph{bad}.  Write
+$\mathcal{C} \subseteq \mathcal{K}(R)$ for the set of good colorings.
+\end{defn}
+
+Now suppose $K$ appears in a minimum counterexample $T$, with free
+completion $S \subseteq T$.  Let $T' := T \setminus V(H)$ (the
+``outside''); since $T$ is a minimum counterexample, $T'$ has a
+$4$-coloring, which restricts to some
+$\mathcal{C}' \subseteq \mathcal{K}(R)$.  For $T$ to be a
+counterexample,
+\[
+   \mathcal{C}' \;\subseteq\; \mathcal{K}(R) \setminus \mathcal{C}
+\]
+(otherwise a coloring extending both into $S$ and into $T'$ gives a
+$4$-coloring of all of $T$).  The goal of reducibility is to show
+$\mathcal{C}' = \emptyset$, contradicting that $T'$ is colorable.
+
+\begin{defn}[Reducibility, classical taxonomy]
+\hfill
+\begin{itemize}
+  \item[A] $K$ is \textbf{A-reducible} if $\mathcal{C} = \mathcal{K}(R)$
+        (every ring coloring extends).  A-reducibility immediately gives
+        $\mathcal{C}' = \emptyset$, but is too strong to hold for any
+        nontrivial configuration.
+  \item[D] $K$ is \textbf{D-reducible} if every bad coloring
+        $\varphi \in \mathcal{K}(R) \setminus \mathcal{C}$ can be
+        transformed --- via a sequence of Kempe-chain swaps on $T'$ ---
+        into a good coloring.  D-reducibility is checkable by computer
+        on $\mathcal{K}(R)$ alone (no knowledge of $T'$ beyond that it
+        is $4$-colorable), because the Kempe-swap closure operation
+        can be applied at the level of ring colorings.
+  \item[C] $K$ is \textbf{C-reducible} if it is D-reducible \emph{after}
+        replacing $H$ by a smaller graph $H'$ (obtained from $H$ by
+        contracting up to four edges in RSST).  This is strictly more
+        powerful than D-reducibility.
+\end{itemize}
+\end{defn}
+
+Birkhoff's diamond (4 mutually adjacent pentagons surrounded by a
+$6$-cycle ring) was the first nontrivial D-reducible configuration:
+of the 31 ring colorings up to $S_4$-symmetry, 16 are good directly,
+and the other 15 each admit a Kempe-swap to a good one.
+
+\subsection*{Discharging and unavoidability}
+
+Reducibility tells you that \emph{if} a good configuration appears in
+$T$, then $T$ is not a counterexample.  The other half of the proof
+is to show that some good configuration \emph{must} appear:
+
+\begin{defn}[Unavoidable set]
+A set $\mathcal{U}$ of configurations is \emph{unavoidable} if every
+internally $6$-connected triangulation contains at least one $K \in
+\mathcal{U}$ as a subconfiguration.
+\end{defn}
+
+Heesch's \emph{discharging method} proves unavoidability:
+\begin{enumerate}
+  \item Assign a \emph{charge} $\operatorname{ch}(v) := 6 - \deg(v)$ to each
+        vertex.  By Euler's formula, $\sum_v \operatorname{ch}(v) = 12$ on
+        any triangulation of the sphere.
+  \item Define \emph{discharging rules} that redistribute charge
+        between vertices without changing the total.
+  \item Show that after discharging, no vertex carries positive charge
+        \emph{unless} it lies in (the neighborhood of) some
+        configuration in $\mathcal{U}$.
+  \item Since total charge is $12 > 0$, some positive-charge vertex
+        exists post-discharging, so some configuration in
+        $\mathcal{U}$ must appear.
+\end{enumerate}
+
+The two halves combine: 4CT $=$ ``every reducible configuration in
+$\mathcal{U}$ blocks counterexamples'' $+$ ``$\mathcal{U}$ is unavoidable.''
+
+\subsection*{The proofs}
+
+\begin{itemize}
+  \item \textbf{Appel--Haken (1976/77).}  $|\mathcal{U}| = 1936$
+        configurations (later reduced to $1482$); $487$ discharging
+        rules.  Computer verification needed.
+  \item \textbf{RSST (1997).} $|\mathcal{U}| = 633$ configurations; $32$
+        discharging rules; quadratic-time $4$-coloring algorithm.
+        Still computer-assisted, but the unavoidability part was
+        written in a formal language and machine-checked.
+\end{itemize}
+
+For configurations of ring-size $r$, the number of colorings of $R$
+modulo $S_4$ is roughly $3^{r-1}/3 + O(2^r)$ from the standard
+chromatic-polynomial formula for $C_r$.  RSST's largest ring-size is
+$14$, with $\sim\!200{,}000$ ring colorings per configuration to
+check.
+
+\section*{Part II: dictionary to the fiber-decomposition view}
+
+\subsection*{Side-of-the-duality conventions}
+
+Our work is on the \emph{edge} side of Tait: we color edges of $G'$
+with $3$ colors, where $G'$ is essentially the dual of a triangulation
+$G$.  Birkhoff--Heesch is on the \emph{vertex} side of $G$.  By Tait's
+theorem these are equivalent in principle, but the shape of a
+``configuration boundary'' looks different on the two sides:
+\begin{center}
+\begin{tabular}{>{\raggedright\arraybackslash}p{0.36\textwidth}|>{\raggedright\arraybackslash}p{0.55\textwidth}}
+\textbf{Vertex side (Birkhoff--Heesch)} & \textbf{Edge side (us)} \\ \hline
+Triangulation $T$ & Cubic dual $G'$ \\
+Configuration $K = (H, \gamma)$ in $T$ & Tire annular face connector
+   $T'_{f'} \subseteq G'$ \\
+Inner-face triangles of $H$ & Vertices of $V(f')$ (dual to annular
+   faces of the tire) \\
+Ring $R$ (a cycle around $H$) & Boundary of $T'_{f'}$, consisting of
+   spoke edges $E_S$ \emph{plus} (in the multi-tire chain) the cycle
+   $V(f')$ itself \\
+Ring coloring $\varphi : V(R) \to \{1,2,3,4\}$ & Spoke configuration
+   $\sigma : E_S \to \{1,2,3\}$ \\
+$\mathcal{K}(R)$ = all proper $4$-colorings of $R$ &
+   $\Sigma := $ all spoke configurations $\sigma$ (whether
+   realisable or not) \\
+$\mathcal{C}$ = good (extendable to $H \cup R$) ring colorings &
+   Realisable spoke configurations:
+   $\{\sigma : N(T'_{f'}; \sigma) > 0\}$ \\
+$\mathcal{K}(R) \setminus \mathcal{C}$ = bad ring colorings &
+   Unrealisable $\sigma$: the boundary of $T'_{f'}$'s reachability \\
+Fiber over a ring coloring: \# extensions of $\varphi$ to $H \cup R$ &
+   Fiber count $N(T'_{f'}; \sigma)$ \\
+Kempe-chain swap on $T \setminus V(H)$ &
+   Tait-Kempe swap on $G' \setminus V(T'_{f'})$ (two-color
+   alternating-edge swap)
+\end{tabular}
+\end{center}
+
+\subsection*{The fiber identity, in Birkhoff language}
+
+Our identity
+$P_e(T'_{f'}, 3) = \sum_\sigma N(T'_{f'}; \sigma)$
+is literally Birkhoff's ``good colorings'' decomposition on the edge
+side, with \emph{the same scaffold}: count interior extensions
+fibered over boundary state.  The classical literature does not
+emphasise this identity per se (it's the trivial sum), but every
+reducibility analysis is built around the fiber distribution
+$\{N(T'_{f'}; \sigma)\}_\sigma$.
+
+\subsection*{What ``reducible'' means in our world}
+
+Translating definitions of A-, D-, C-reducibility through the
+dictionary:
+
+\begin{itemize}
+  \item \textbf{Edge-A-reducibility of $T'_{f'}$}: every spoke
+        configuration $\sigma \in \Sigma$ is realisable.  This would
+        mean $T'_{f'}$ supports an edge $3$-coloring extension from
+        \emph{any} boundary input --- a very strong locally-flexible
+        property.
+  \item \textbf{Edge-D-reducibility of $T'_{f'}$}: every unrealisable
+        $\sigma$ can be Tait-Kempe-swapped (in the outside graph
+        $G' \setminus T'_{f'}$) to a realisable one.  This is the
+        natural form of the conductivity step from our chain-pigeonhole
+        sketch.
+  \item \textbf{Edge-C-reducibility of $T'_{f'}$}: D-reducibility
+        after replacing $T'_{f'}$ by a smaller subgraph (e.g.\
+        contracting some spoke edges or merging adjacent faces).
+\end{itemize}
+
+\subsection*{The chain-pigeonhole step as a reducibility statement}
+
+Our conductivity step --- ``the middle tire $T_B$'s
+$\phi_B : \mathcal{P}_{AB} \to 2^{\mathcal{P}_{BC}}$ takes any input
+to a $>\!|\mathcal{P}_{BC}|/2$-sized output'' --- is the
+\emph{quantitative} analogue of D-reducibility, but applied to
+\emph{composition} of configurations rather than reduction.  In
+particular:
+
+\begin{itemize}
+  \item Birkhoff--Heesch D-reducibility says ``bad inputs to a single
+        configuration can be Kempe-moved to good ones.''
+  \item Our chain-pigeonhole says ``the bad inputs to the inner tire
+        and the bad inputs to the outer tire together don't cover
+        $\mathcal{P}_\gamma$, so something good remains.''
+\end{itemize}
+
+These are not the same statement, but they are about the same data
+$\mathcal{C}$ vs.\ $\mathcal{K} \setminus \mathcal{C}$ on the shared
+cycle.
+
+\section*{Part III: does the machinery apply?}
+
+\subsection*{What carries over cleanly}
+
+\begin{enumerate}
+  \item \textbf{Vocabulary and scaffolding.}  Configurations,
+        rings, free completions, color sets, fiber-of-extensions are
+        all there; the menagerie/fiber notes are using the same
+        objects.
+  \item \textbf{Kempe-chain machinery.}  Tait-Kempe chains (two-color
+        alternating edge paths in $G'$) are a real, well-developed
+        tool.  Any conductivity argument we want is fundamentally
+        Tait-Kempe in flavour.
+  \item \textbf{Computer-verifiability for small tires.}  Just as
+        D-reducibility of an individual configuration is verified by
+        enumerating $\sim\!200{,}000$ ring colorings, the fiber
+        distribution $\{N(T'_{f'}; \sigma)\}$ for a fixed small tire
+        is a finite Sage computation.  We can test conductivity
+        empirically before trying to prove it.
+\end{enumerate}
+
+\subsection*{What does \emph{not} carry over straightforwardly}
+
+\begin{enumerate}
+  \item \textbf{The reducibility scale.}  Classical reducibility was
+        only ever practical for ring-size $\leq 14$ because the number
+        of ring colorings explodes.  Our tires can have arbitrarily
+        large boundary cycles (in a multi-layer triangulation, the
+        annular ring is whatever the level structure gives), so the
+        \emph{single-configuration} reducibility approach hits the
+        same wall as A\&H/RSST: only small tires are tractable
+        directly.
+  \item \textbf{Compositionality.}  Birkhoff--Heesch operates on
+        \emph{one} configuration at a time.  Our chain
+        pigeonhole/nesting is fundamentally about \emph{composing}
+        configurations along shared boundaries.  This is a structural
+        feature classical reducibility does \emph{not} engage with ---
+        their unavoidability argument (discharging) replaces it.  If
+        we want to prove a statement of the form ``every nested chain
+        of tires admits a global $4$-coloring,'' Birkhoff--Heesch does
+        not directly give us the tool; we need either a transfer-matrix
+        / monotonicity argument across nestings or a structural
+        result about how the realisable supports behave under
+        composition.
+  \item \textbf{Unavoidability is automatic / different.}  In 4CT,
+        unavoidability is a separate hard problem solved by
+        discharging.  In our setup the tire decomposition of
+        $G$ is given by the level structure (Bauerfeld
+        \cite{bauerfeld-pds}), so there is no analogous unavoidability
+        question --- the tires are already there.  This means
+        \emph{half} of the classical apparatus (discharging) is not
+        the point of contact; the contact is purely on the
+        reducibility/color-set side.
+  \item \textbf{Tait correspondence is global, not local.}  Edge
+        $3$-coloring of $G'$ globally encodes a vertex $4$-coloring of
+        $G$, but the local correspondence between an edge coloring of
+        $T'_{f'}$ and a vertex coloring of the corresponding piece of
+        $G$ is subtle: edge swaps on the dual side do not always
+        correspond to single Kempe chains on the primal side, and the
+        ``ring'' as a vertex cycle in $G$ may differ in length and
+        structure from the ``boundary'' of $T'_{f'}$ on the edge side.
+        Any time we want to import a vertex-side Kempe argument we
+        will have to do the bookkeeping carefully.
+\end{enumerate}
+
+\subsection*{Assessment}
+
+\textbf{Yes, the Birkhoff--Heesch framework applies, but only as a
+language and as a verification tool for small instances.}  It does
+\emph{not} hand us a proof of the nesting/chain-pigeonhole conjecture
+for free, because:
+\begin{itemize}
+  \item Classical reducibility is single-configuration; our argument
+        is multi-configuration / compositional.
+  \item Classical reducibility's quantitative input is exhaustive
+        enumeration of ring colorings up to size $14$; we want
+        statements uniform over arbitrarily large tires.
+\end{itemize}
+
+What it \emph{does} hand us:
+\begin{itemize}
+  \item A precise vocabulary --- good/bad colorings, free completion,
+        D-/C-reducibility --- so that the conductivity step can be
+        stated in established terms.
+  \item A concrete computational template: for any specific tire,
+        compute $\{N(T'_{f'}; \sigma)\}_\sigma$ in Sage and check
+        whether the realisable support $\mathcal{C}$ is large enough
+        that two adjacent tires must overlap.  This is the
+        analogue of mechanical D-reducibility checking.
+  \item Strong evidence about the difficulty: nothing in 80+ years of
+        reducibility work has reduced 4CT to a structural argument
+        across all configuration sizes.  If our chain argument
+        succeeds, it will be \emph{because tires are a more
+        structured class than arbitrary configurations}, not because
+        the reducibility apparatus suddenly gives uniform results.
+\end{itemize}
+
+\subsection*{Concrete next steps}
+
+\begin{enumerate}
+  \item \textbf{Pick a small tire family} ($B_{\mathrm{in}}$ a $k$-cycle
+        for $k \in \{3, 4, 5, 6\}$, $B_{\mathrm{out}}$ a small cycle,
+        no $O$-chords) and compute the full fiber distribution
+        $\{N(T'_{f'}; \sigma)\}_\sigma$ in Sage.  This gives the realisable
+        support $\mathcal{C}$ and, in classical terms, tests whether
+        small tires are A-reducible (full support), D-reducible
+        (Kempe-recoverable), or neither.
+  \item \textbf{Check support overlap for adjacent tires.}  Given two
+        small tires sharing a cycle $\gamma$, do the realisable
+        supports $\mathcal{C}_{\mathrm{out}}, \mathcal{C}_{\mathrm{in}}
+        \subseteq \mathcal{K}(\gamma)$ always intersect?  This is the
+        empirical version of the chain-pigeonhole step.  If they
+        sometimes miss, the simple form of the argument fails and
+        we need a Kempe-chain (D-reducibility-style) escape route.
+  \item \textbf{Look up monosystems / Tutte.}  Tutte
+        \cite{tutte-chromial} formulated 4CT-adjacent counting
+        problems in terms of his \emph{chromial}; this is the closest
+        existing transfer-matrix-style framing of these color sets,
+        and may give a cleaner composition rule than the raw fiber
+        sum.
+  \item \textbf{Look up Sokal / Chang--Shrock} on chromatic
+        polynomials of strip graphs.  They use transfer matrices for
+        infinite families of small-ring configurations, which is
+        structurally similar to nested tires with fixed ring size.
+\end{enumerate}
+
+\begin{thebibliography}{9}
+
+\bibitem{birkhoff}
+G.~D.~Birkhoff,
+\emph{The reducibility of maps},
+Amer.\ J.\ Math.\ \textbf{35} (1913), 115--128.
+
+\bibitem{heesch}
+H.~Heesch,
+\emph{Untersuchungen zum Vierfarbenproblem},
+B.~I.\ Hochschulskripten 810/810a/810b, Bibliographisches Institut,
+Mannheim, 1969.
+
+\bibitem{appel-haken}
+K.~Appel and W.~Haken,
+\emph{Every planar map is four colorable. Part I: Discharging};
+\emph{Part II: Reducibility} (with J.~Koch),
+Illinois J.\ Math.\ \textbf{21} (1977), 429--567.
+
+\bibitem{rsst}
+N.~Robertson, D.~P.~Sanders, P.~Seymour, R.~Thomas,
+\emph{The Four-Colour Theorem},
+J.\ Combin.\ Theory Ser.\ B \textbf{70} (1997), 2--44.
+
+\bibitem{thomas-update}
+R.~Thomas,
+\emph{An update on the Four-Color Theorem},
+Notices Amer.\ Math.\ Soc.\ \textbf{45} (1998), 848--859.
+
+\bibitem{tutte-chromial}
+W.~T.~Tutte,
+\emph{Chromials},
+in: \emph{Hypergraph Seminar} (C.~Berge, D.~Ray-Chaudhuri, eds.),
+Lecture Notes in Math.\ 411, Springer, 1974, pp.~243--266.
+
+\bibitem{bauerfeld-pds}
+E.~Bauerfeld,
+\emph{Plane Depth Sequencing},
+manuscript (math-research repository), 2026.
+
+\end{thebibliography}
+
+\end{document}