Add double-contraction reductio strategy note

Records the degree-5 double-contraction proof skeleton: Kempe chains as Heawood face-chains (flip-set + same-side sign rule), the chain-transport hypothesis L1, the inner/outer nested reductio, H'' as per-interface contraction along the chain, and the single emptiness Claim it reduces to, with the Errera oracle as the stress test. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
2026-06-18 23:43:45 -04:00
parent 5552e07803
commit f54b66f857
4 changed files with 438 additions and 0 deletions
@@ -0,0 +1,4 @@
+\relax 
+\@writefile{toc}{\contentsline {paragraph}{Inner.}{2}{}\protected@file@percent }
+\@writefile{toc}{\contentsline {paragraph}{Outer.}{2}{}\protected@file@percent }
+\gdef \@abspage@last{2}
@@ -0,0 +1,296 @@
+This is pdfTeX, Version 3.141592653-2.6-1.40.24 (TeX Live 2022) (preloaded format=pdflatex 2022.10.5)  18 JUN 2026 23:27
+entering extended mode
+ restricted \write18 enabled.
+ %&-line parsing enabled.
+**double_contraction_reductio.tex
+(./double_contraction_reductio.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/booktabs/booktabs.sty
+Package: booktabs 2020/01/12 v1.61803398 Publication quality tables
+\heavyrulewidth=\dimen158
+\lightrulewidth=\dimen159
+\cmidrulewidth=\dimen160
+\belowrulesep=\dimen161
+\belowbottomsep=\dimen162
+\aboverulesep=\dimen163
+\abovetopsep=\dimen164
+\cmidrulesep=\dimen165
+\cmidrulekern=\dimen166
+\defaultaddspace=\dimen167
+\@cmidla=\count274
+\@cmidlb=\count275
+\@aboverulesep=\dimen168
+\@belowrulesep=\dimen169
+\@thisruleclass=\count276
+\@lastruleclass=\count277
+\@thisrulewidth=\dimen170
+)
+(/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=\count278
+\l__pdf_internal_box=\box52
+)
+No file double_contraction_reductio.aux.
+\openout1 = `double_contraction_reductio.aux'.
+
+LaTeX Font Info:    Checking defaults for OML/cmm/m/it on input line 20.
+LaTeX Font Info:    ... okay on input line 20.
+LaTeX Font Info:    Checking defaults for OMS/cmsy/m/n on input line 20.
+LaTeX Font Info:    ... okay on input line 20.
+LaTeX Font Info:    Checking defaults for OT1/cmr/m/n on input line 20.
+LaTeX Font Info:    ... okay on input line 20.
+LaTeX Font Info:    Checking defaults for T1/cmr/m/n on input line 20.
+LaTeX Font Info:    ... okay on input line 20.
+LaTeX Font Info:    Checking defaults for TS1/cmr/m/n on input line 20.
+LaTeX Font Info:    ... okay on input line 20.
+LaTeX Font Info:    Checking defaults for OMX/cmex/m/n on input line 20.
+LaTeX Font Info:    ... okay on input line 20.
+LaTeX Font Info:    Checking defaults for U/cmr/m/n on input line 20.
+LaTeX Font Info:    ... okay on input line 20.
+(/usr/local/texlive/2022/texmf-dist/tex/context/base/mkii/supp-pdf.mkii
+[Loading MPS to PDF converter (version 2006.09.02).]
+\scratchcounter=\count279
+\scratchdimen=\dimen171
+\scratchbox=\box53
+\nofMPsegments=\count280
+\nofMParguments=\count281
+\everyMPshowfont=\toks29
+\MPscratchCnt=\count282
+\MPscratchDim=\dimen172
+\MPnumerator=\count283
+\makeMPintoPDFobject=\count284
+\everyMPtoPDFconversion=\toks30
+) (/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)
+
+LaTeX Font Info:    Trying to load font information for U+msa on input line 21.
+
+(/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 21.
+
+
+(/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]
+(./double_contraction_reductio.aux) ) 
+Here is how much of TeX's memory you used:
+ 3256 strings out of 478268
+ 48463 string characters out of 5846347
+ 347695 words of memory out of 5000000
+ 21442 multiletter control sequences out of 15000+600000
+ 479484 words of font info for 65 fonts, out of 8000000 for 9000
+ 1141 hyphenation exceptions out of 8191
+ 55i,5n,62p,244b,218s stack positions out of 10000i,1000n,20000p,200000b,200000s
+{/usr/local/texlive/2022/texmf-dist/fonts/
+enc/dvips/cm-super/cm-super-ts1.enc}</usr/local/texlive/2022/texmf-dist/fonts/t
+ype1/public/amsfonts/cm/cmbx10.pfb></usr/local/texlive/2022/texmf-dist/fonts/ty
+pe1/public/amsfonts/cm/cmbx12.pfb></usr/local/texlive/2022/texmf-dist/fonts/typ
+e1/public/amsfonts/cm/cmbxti10.pfb></usr/local/texlive/2022/texmf-dist/fonts/ty
+pe1/public/amsfonts/cm/cmitt10.pfb></usr/local/texlive/2022/texmf-dist/fonts/ty
+pe1/public/amsfonts/cm/cmmi10.pfb></usr/local/texlive/2022/texmf-dist/fonts/typ
+e1/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/type1/p
+ublic/amsfonts/cm/cmr17.pfb></usr/local/texlive/2022/texmf-dist/fonts/type1/pub
+lic/amsfonts/cm/cmr8.pfb></usr/local/texlive/2022/texmf-dist/fonts/type1/public
+/amsfonts/cm/cmss8.pfb></usr/local/texlive/2022/texmf-dist/fonts/type1/public/a
+msfonts/cm/cmsy10.pfb></usr/local/texlive/2022/texmf-dist/fonts/type1/public/am
+sfonts/cm/cmsy8.pfb></usr/local/texlive/2022/texmf-dist/fonts/type1/public/amsf
+onts/cm/cmti10.pfb></usr/local/texlive/2022/texmf-dist/fonts/type1/public/amsfo
+nts/symbols/msam10.pfb></usr/local/texlive/2022/texmf-dist/fonts/type1/public/c
+m-super/sfrm1095.pfb>
+Output written on double_contraction_reductio.pdf (2 pages, 176278 bytes).
+PDF statistics:
+ 87 PDF objects out of 1000 (max. 8388607)
+ 52 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)
+
@@ -0,0 +1,138 @@
+\documentclass[11pt]{article}
+\usepackage{amsmath,amssymb,amsthm}
+\usepackage{graphicx}
+\usepackage{geometry}
+\usepackage{booktabs}
+\geometry{margin=1in}
+
+\title{A double-contraction reductio at a degree-5 vertex\\
+via Kempe chains as Heawood face-chains}
+\author{}
+\date{}
+
+\newtheorem*{obs}{Observation}
+\newtheorem*{prop}{Proposition}
+\newtheorem*{conj}{Conjecture}
+\newtheorem*{lem}{Lemma}
+\newtheorem*{claim}{Claim}
+\newtheorem*{remk}{Remark}
+
+\begin{document}
+\maketitle
+
+\emph{Status: exploratory strategy note. Records a proof skeleton and the
+single lemma it reduces to; nothing here is proved. Companion to
+\texttt{boundary\_restriction\_structure.tex} and \texttt{paper.tex}.}
+
+\section*{Setup: the move}
+
+Let $G$ be a minimal counterexample to the Four Colour Theorem (a smallest
+triangulation with no proper $4$-vertex-colouring). By Euler $G$ has a
+vertex $v$ of degree $\le 5$; degrees $\le 4$ are classically reducible, so
+take $\deg(v)=5$. The link of $v$ is a pentagon $a,x,b,y,z$ (consecutive
+neighbours adjacent). For a non-adjacent (diagonal) pair, say $a,b$, the
+\emph{double contraction} contracts both edges $(a,v)$ and $(b,v)$,
+identifying $a=v=b$ into a single vertex. There are $5$ diagonal pairs.
+
+The double contraction is a proper minor with two fewer vertices, hence a
+smaller planar graph $G'$; by minimality $G'$ is $4$-colourable. It stays a
+simple triangulation iff each contracted edge is non-separating (its
+endpoints have exactly two common neighbours).
+
+\section*{Kempe chains as Heawood face-chains}
+
+Work in the cubic dual $G'$ (vertices $=$ faces of $G$, so the Heawood
+$\pm1$ labels sit on dual vertices). Tait-colour the edges with the three
+nonzero Klein-4 elements $\{a,b,c\}$ (edge colour $=$ colour-difference
+across the primal edge). Then:
+
+\begin{obs}[Kempe chain $=$ Tait cycle $=$ flip-set]
+A primal Kempe chain (component of two vertex-colour classes of $G$)
+corresponds to a connected component of the two-edge-colour subgraph
+$\{a,b\}$ of the dual. That subgraph is $2$-regular, so it is a disjoint
+union of cycles; each such cycle alternates $a,b,a,b,\dots$ and is therefore
+\textbf{always even}. The cycle is literally a cyclic chain of faces of $G$.
+A Kempe swap reverses the rotational order $(a,b,c)$ at exactly the vertices
+on the cycle, so the set of faces whose Heawood sign \emph{flips} under the
+swap is precisely the Kempe chain.
+\end{obs}
+
+\begin{obs}[Sign alternation $=$ same-side rule]
+Even-ness does \emph{not} force the Heawood signs to alternate along the
+cycle. At each cycle vertex the third (off-cycle, colour-$c$) edge points
+either inside or outside the region bounded by the cycle. For consecutive
+vertices $A,B$:
+\[
+  \text{same side (both in / both out)} \Rightarrow \text{signs flip;}
+  \qquad
+  \text{opposite side} \Rightarrow \text{signs repeat.}
+\]
+(Local chirality computation: the four in/out cases give
+$+,-$ / $-,+$ / $+,+$ / $-,-$.) Hence the Heawood sign sequence around a
+Tait cycle is determined, up to one global sign, by the in/out pattern of
+the third edges; it is fully alternating iff there are zero side-switches,
+i.e.\ all third edges lie on one side.
+\end{obs}
+
+\section*{The transport hypothesis (L1)}
+
+\begin{conj}[Chain transport, claimed for all triangulations]
+The double contraction preserves the relevant (crossing) Kempe/Heawood
+chain structure as it propagates up the nested tire decomposition: the two
+chains anchored at the pentagon survive, consistently, through every tire
+interface above $v$.
+\end{conj}
+
+\section*{The reductio (two nested contradictions)}
+
+We are \emph{not} claiming $G'$ is uncolourable, and we are not claiming
+intertwined Kempe chains are impossible (they occur, e.g.\ in the Errera
+graph). The reducible object is \emph{forced} intertwining.
+
+\paragraph{Inner.} Suppose intertwining is the \emph{only} way to colour
+$G'$ (every colouring is intertwined at $v$). By transport the two crossing
+chains pass through every interface above; if uncrossing is excluded at each
+interface, the tire restriction relations $R_{\mathsf K}$ collapse to their
+``crossed-only'' sub-relations. Contract each interface \textbf{along the
+chain} to obtain a strictly smaller triangulation $H''$. If the crossed-only
+sub-relations admit no compatible gluing on $H''$, then $H''$ is
+uncolourable and smaller than $G$ --- contradicting minimality.
+
+\paragraph{Outer.} Therefore $G'$ admits a non-intertwined colouring; it
+uncrosses at $v$, frees a colour for $v$, and lifts to a colouring of $G$ ---
+contradicting that $G$ is a counterexample. \hfill$\square$ (modulo the
+lemma below)
+
+\section*{What it all reduces to}
+
+\begin{claim}[the only open content]
+Under the crossed-only collapse, the surviving Heawood boundary sequences at
+a (forced-short) tire interface have empty pointwise-negation gluing on
+$H''$ --- not merely small, genuinely empty.
+\end{claim}
+
+This is where the $2^{n-2}$ constraint floor and the mod-3 side-pattern must
+do real work: the floor guarantees that \emph{smallness alone} never empties
+a relation, so the emptiness must come from the chains pinning the
+sub-relation down, not from short interface length.
+
+\section*{Open points / to pin next}
+
+\begin{itemize}
+\item \textbf{Define $H''$ precisely.} Current candidate: contract each tire
+  interface along the transported chain (the global analogue of the local
+  double contraction). Confirm this is a definite, strictly smaller
+  triangulation.
+\item \textbf{Lift is not automatic.} ``Non-intertwined'' must be defined as
+  ``admits a swap collapsing the pentagon $a,x,b,y,z$ to $\le 3$ colours,''
+  or freeing $v$ fails even after uncrossing (with $c(a)=c(b)$ the pentagon
+  can still show $4$ colours).
+\item \textbf{Errera oracle.} Run the whole construction against the Errera
+  graph (and Fritsch / Kittell). These are colourable but Kempe-intertwined;
+  the hypothesis ``every colouring intertwined'' must \emph{fail} for them,
+  so the construction must decline. \emph{Why} it declines is exactly the
+  mechanism the Claim must deny in the counterexample case.
+\item \textbf{Prove or break L1} as a statement about all triangulations.
+\end{itemize}
+
+\end{document}