coloring_nested_tire_graphs: rainbow theorem proof (sharp threshold + 2-SAT reduction)

Replaces the earlier proof sketch with a clearer attempt that: 1. Corrects the sharp threshold: m_1 >= m - 1 (not m_1 >= m). Empirically verified for m ∈ {4, 6} across m_1 ≥ m - 1. 2. Proves the ⊆ direction cleanly: each O-face dual vertex has degree m/2 ≤ 3 in T'_{f'}, so its incident spokes must be pairwise distinct, putting σ in the "perms-per-half" set P_m. 3. Reduces the ⊇ direction to a cyclic 2-SAT solvability claim (Conjecture 2sat): for each σ ∈ P_m, find an "orientation" o ∈ {0,1}^m at the m D-positions such that each length-1 gap has R_j = L_{j+1} and each length-2 gap has R_j ≠ L_{j+1}. 4. Acknowledges the gap: a naive "all-zero orientation" fails (e.g. rainbow at m_1 = 6 has the all-zero attempt fail at gap (4,5)). A satisfying assignment exists in every tested case (6-18 per σ at m=6, m_1=6) but a clean general proof awaits. Two routes outlined: S_3-equivariant case analysis, or global implication-graph analysis. 5. Confirms sharpness with explicit forcing-propagation counterexample at m=6, m_1=4 (rainbow not in π_D). 6. States provisional corollary: π_D = P_m at m_1 ≥ m - 1 (conditional on Conjecture 2sat); chain pigeonhole reduces to π_U meeting P_m. Honest about what's proven (the ⊆ half, the 2-SAT reduction, the sharpness counterexample) and what's left (the 2-SAT solvability proof). Note: rainbow_proof.tex (4 pages). Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com>
2026-05-26 04:18:00 -04:00
parent c900ec9a70
commit 56ebf49b48
4 changed files with 597 additions and 0 deletions
@@ -0,0 +1,10 @@
+\relax 
+\newlabel{thm:rainbow}{{1}{1}}
+\newlabel{lem:o-face}{{2}{1}}
+\newlabel{lem:gap}{{3}{2}}
+\newlabel{prop:reduction}{{4}{2}}
+\newlabel{conj:2sat}{{5}{2}}
+\newlabel{prop:sharpness}{{6}{3}}
+\newlabel{cor:provisional}{{7}{3}}
+\newlabel{cor:chain}{{8}{3}}
+\gdef \@abspage@last{4}
@@ -0,0 +1,308 @@
+This is pdfTeX, Version 3.141592653-2.6-1.40.24 (TeX Live 2022) (preloaded format=pdflatex 2022.10.5)  26 MAY 2026 04:17
+entering extended mode
+ restricted \write18 enabled.
+ %&-line parsing enabled.
+**rainbow_proof.tex
+(./rainbow_proof.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
+)
+\c@theorem=\count278
+
+(/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=\count279
+\l__pdf_internal_box=\box52
+)
+(./rainbow_proof.aux)
+\openout1 = `rainbow_proof.aux'.
+
+LaTeX Font Info:    Checking defaults for OML/cmm/m/it on input line 22.
+LaTeX Font Info:    ... okay on input line 22.
+LaTeX Font Info:    Checking defaults for OMS/cmsy/m/n on input line 22.
+LaTeX Font Info:    ... okay on input line 22.
+LaTeX Font Info:    Checking defaults for OT1/cmr/m/n on input line 22.
+LaTeX Font Info:    ... okay on input line 22.
+LaTeX Font Info:    Checking defaults for T1/cmr/m/n on input line 22.
+LaTeX Font Info:    ... okay on input line 22.
+LaTeX Font Info:    Checking defaults for TS1/cmr/m/n on input line 22.
+LaTeX Font Info:    ... okay on input line 22.
+LaTeX Font Info:    Checking defaults for OMX/cmex/m/n on input line 22.
+LaTeX Font Info:    ... okay on input line 22.
+LaTeX Font Info:    Checking defaults for U/cmr/m/n on input line 22.
+LaTeX Font Info:    ... okay on input line 22.
+
+(/usr/local/texlive/2022/texmf-dist/tex/context/base/mkii/supp-pdf.mkii
+[Loading MPS to PDF converter (version 2006.09.02).]
+\scratchcounter=\count280
+\scratchdimen=\dimen171
+\scratchbox=\box53
+\nofMPsegments=\count281
+\nofMParguments=\count282
+\everyMPshowfont=\toks29
+\MPscratchCnt=\count283
+\MPscratchDim=\dimen172
+\MPnumerator=\count284
+\makeMPintoPDFobject=\count285
+\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 23.
+
+(/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 23.
+
+
+(/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]
+Overfull \hbox (4.14233pt too wide) in paragraph at lines 213--220
+[]\OT1/cmr/m/n/10.95 A clean proof of Con-jec-ture 5[] likely pro-ceeds by: (i)
+ Show-ing the im-pli-ca-tion graph on $\OMS/cmsy/m/n/10.95 f\OT1/cmr/m/n/10.95 
+(\OML/cmm/m/it/10.95 o[]; o[]\OT1/cmr/m/n/10.95 )\OMS/cmsy/m/n/10.95 g$
+ []
+
+[3] [4] (./rainbow_proof.aux) ) 
+Here is how much of TeX's memory you used:
+ 3279 strings out of 478268
+ 48627 string characters out of 5846347
+ 352821 words of memory out of 5000000
+ 21466 multiletter control sequences out of 15000+600000
+ 480828 words of font info for 72 fonts, out of 8000000 for 9000
+ 1141 hyphenation exceptions out of 8191
+ 55i,8n,62p,230b,218s stack positions out of 10000i,1000n,20000p,200000b,200000s
+{/usr/local/texlive/2022/texmf-dist/fonts/enc/dv
+ips/cm-super/cm-super-ts1.enc}</usr/local/texlive/2022/texmf-dist/fonts/type1/p
+ublic/amsfonts/cm/cmbx10.pfb></usr/local/texlive/2022/texmf-dist/fonts/type1/pu
+blic/amsfonts/cm/cmbx12.pfb></usr/local/texlive/2022/texmf-dist/fonts/type1/pub
+lic/amsfonts/cm/cmex10.pfb></usr/local/texlive/2022/texmf-dist/fonts/type1/publ
+ic/amsfonts/cm/cmmi10.pfb></usr/local/texlive/2022/texmf-dist/fonts/type1/publi
+c/amsfonts/cm/cmmi12.pfb></usr/local/texlive/2022/texmf-dist/fonts/type1/public
+/amsfonts/cm/cmmi6.pfb></usr/local/texlive/2022/texmf-dist/fonts/type1/public/a
+msfonts/cm/cmmi8.pfb></usr/local/texlive/2022/texmf-dist/fonts/type1/public/ams
+fonts/cm/cmr10.pfb></usr/local/texlive/2022/texmf-dist/fonts/type1/public/amsfo
+nts/cm/cmr12.pfb></usr/local/texlive/2022/texmf-dist/fonts/type1/public/amsfont
+s/cm/cmr17.pfb></usr/local/texlive/2022/texmf-dist/fonts/type1/public/amsfonts/
+cm/cmr6.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/cms
+y10.pfb></usr/local/texlive/2022/texmf-dist/fonts/type1/public/amsfonts/cm/cmsy
+6.pfb></usr/local/texlive/2022/texmf-dist/fonts/type1/public/amsfonts/cm/cmsy8.
+pfb></usr/local/texlive/2022/texmf-dist/fonts/type1/public/amsfonts/cm/cmti10.p
+fb></usr/local/texlive/2022/texmf-dist/fonts/type1/public/amsfonts/cm/cmtt10.pf
+b></usr/local/texlive/2022/texmf-dist/fonts/type1/public/cm-super/sfrm1095.pfb>
+
+Output written on rainbow_proof.pdf (4 pages, 221653 bytes).
+PDF statistics:
+ 108 PDF objects out of 1000 (max. 8388607)
+ 65 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,279 @@
+\documentclass[11pt]{article}
+\usepackage{amsmath,amssymb,amsthm}
+\usepackage{graphicx}
+\usepackage{geometry}
+\usepackage{booktabs}
+\geometry{margin=1in}
+
+\title{Towards a proof of the antipodal-chord rainbow theorem\\
+       (corrected statement with sharp threshold)}
+\author{}
+\date{}
+
+\theoremstyle{plain}
+\newtheorem{theorem}{Theorem}
+\newtheorem{lemma}[theorem]{Lemma}
+\newtheorem{prop}[theorem]{Proposition}
+\newtheorem{cor}[theorem]{Corollary}
+\newtheorem{conj}[theorem]{Conjecture}
+\theoremstyle{definition}
+\newtheorem{defn}[theorem]{Definition}
+
+\begin{document}
+\maketitle
+
+\section*{Statement and status}
+
+\begin{theorem}[Antipodal-chord rainbow theorem, claimed]
+\label{thm:rainbow}
+Let $T = T(m_1, m)$ be a tire whose outer boundary $B_{\mathrm{out}}$
+has length $m_1$, whose inner boundary $B_{\mathrm{in}}$ has even
+length $m \in \{4, 6\}$, and whose inner outerplanar graph is
+$O = B_{\mathrm{in}} \cup \{(v_0, v_{m/2})\}$ (the antipodal chord).
+Assume the Steiner-poor model and the balanced annular triangulation.
+
+If $m_1 \geq m - 1$, then
+\[
+   \pi_D(\mathcal{C}(T))
+   \;=\;
+   \mathcal{P}_m
+   \;:=\;
+   \bigl\{\sigma \in \{1,2,3\}^m :\;
+   (\sigma_0, \dots, \sigma_{m/2 - 1}),\;
+   (\sigma_{m/2}, \dots, \sigma_{m-1})
+   \in \mathrm{Perm}(\{1, 2, 3\}^{m/2})\bigr\}.
+\]
+In particular $\pi_D$ contains the $S_3$-orbit of the rainbow
+configuration $(a, b, c, b, c, \dots, b, c, a)$.
+
+The threshold $m_1 \geq m - 1$ is sharp: at $m_1 = m - 2$ (when
+$m = 6$) one has $|\pi_D| = 18$ and the rainbow is missing.
+\end{theorem}
+
+\textbf{Status.}  The ``$\subseteq$'' half is fully proven below.  The
+``$\supseteq$'' half is partially proven --- reduced to a cyclic
+2-SAT solvability statement which is empirically true for every
+$\sigma \in \mathcal{P}_m$ (between 6 and 18 satisfying orientation
+assignments per $\sigma$) but for which a clean general proof is
+deferred.  Sharpness is confirmed by explicit forcing
+counterexamples.
+
+\section*{The easy direction: $\pi_D \subseteq \mathcal{P}_m$}
+
+\begin{lemma}[O-face dual constraint]
+\label{lem:o-face}
+For any $\sigma \in \pi_D(\mathcal{C}(T))$, the restrictions of
+$\sigma$ to the two halves $\{0, \dots, m/2 - 1\}$ and
+$\{m/2, \dots, m - 1\}$ are each permutations of $\{1, 2, 3\}^{m/2}$
+with $m/2$ distinct entries (so $\in \mathrm{Perm}$ when $m/2 = 3$).
+\end{lemma}
+
+\begin{proof}
+The antipodal chord splits $O$ into two faces $F_A, F_B$.  Under SP,
+$F_A$ has boundary $B_{\mathrm{in}}$-edges $e_0, \dots, e_{m/2-1}$
+and $F_B$ has $e_{m/2}, \dots, e_{m-1}$.  In $T'_{f'}$ each face
+dual $u_{F_A}$ has degree exactly $m/2$, with one $D$-spoke per
+$B_{\mathrm{in}}$-edge.  Proper edge $3$-coloring at $u_{F_A}$
+requires all $m/2$ incident spokes to have distinct colors;  since
+we only have $3$ colors and $m/2 \in \{2, 3\}$, this is exactly the
+``$m/2$ distinct entries among $\{1,2,3\}$'' condition. Symmetric
+for $F_B$.
+\end{proof}
+
+Consequently $|\pi_D| \leq |\mathcal{P}_m| = 36$ at both $m = 4$ and
+$m = 6$.
+
+\section*{Reduction of $\mathcal{P}_m \subseteq \pi_D$ to a cyclic
+$2$-SAT}
+
+We work in the balanced annular triangulation with $D$-positions
+$p_j = \lfloor j(m_1 + m)/m \rfloor$ on $T'_{\mathrm{ann}} = C_n$,
+$n := m_1 + m$.
+
+\subsection*{Setup of orientations and gaps}
+
+At each $D$-position $p_j$, the two incident cycle edges
+$(e_{p_j - 1}, e_{p_j})$ are constrained by
+Lemma~\ref{lem:o-face}'s consequence at the cycle vertex $p_j$ to
+satisfy $\{c(e_{p_j - 1}),\, c(e_{p_j})\} =
+\{1, 2, 3\} \setminus \{\sigma_j\} =: \{\alpha_j, \beta_j\}$ with
+$\alpha_j < \beta_j$.  Let $o_j \in \{0, 1\}$ encode the choice:
+\[
+   o_j = 0 \;\Leftrightarrow\;
+   c(e_{p_j - 1}) = \alpha_j,\; c(e_{p_j}) = \beta_j;
+   \qquad
+   o_j = 1 \;\Leftrightarrow\;
+   \text{swapped.}
+\]
+
+Between consecutive $D$-positions $p_j, p_{j+1}$ (cyclically) sit
+$L_j - 1 \geq 0$ $U$-positions, where $L_j := p_{j+1} - p_j$ is the
+gap arc length.  Cycle edges within the gap form a path; the two
+endpoints have already-fixed colors $R_j := c(e_{p_j})$ (right side
+of $p_j$) and $L_{j+1} := c(e_{p_{j+1} - 1})$ (left side of $p_{j+1}$),
+both determined by $o_j$ and $o_{j+1}$ via
+$R_j = \beta_j$ if $o_j = 0$ else $\alpha_j$, and $L_{j+1} =
+\alpha_{j+1}$ if $o_{j+1} = 0$ else $\beta_{j+1}$.
+
+\begin{lemma}[Gap feasibility]
+\label{lem:gap}
+Given $R_j, L_{j+1}$ and gap arc length $L_j \geq 1$, the gap
+admits a proper edge $3$-coloring of its interior cycle edges and
+$U$-spokes iff
+\[
+   L_j = 1 \;\Rightarrow\; R_j = L_{j+1};
+   \qquad
+   L_j = 2 \;\Rightarrow\; R_j \neq L_{j+1};
+   \qquad
+   L_j \geq 3 \;\Rightarrow\; \text{no constraint}.
+\]
+For $L_j \geq 3$ at least one extension exists (chromatic-polynomial
+nonzero).
+\end{lemma}
+
+\begin{proof}
+$L_j = 1$: a unique cycle edge equals both $R_j$ and $L_{j+1}$ (it
+\emph{is} the edge connecting them).  $L_j = 2$: two adjacent edges
+with fixed endpoints $R_j, L_{j+1}$ require $R_j \neq L_{j+1}$ for
+proper coloring at the $U$-position between.  $L_j \geq 3$:
+straightforward to construct any pair $(R_j, L_{j+1})$ by alternating
+colors with at least one ``flexible'' cycle edge between.
+\end{proof}
+
+\subsection*{Reduction to cyclic 2-SAT}
+
+When $m_1 \geq m$, every $L_j \geq 2$; when $m_1 = m - 1$, exactly
+one $L_j = 1$ (with the rest $L_j = 2$).
+
+\begin{prop}[2-SAT reduction]
+\label{prop:reduction}
+For $\sigma \in \mathcal{P}_m$, the existence of a proper edge
+$3$-coloring of $T'_{f'}$ inducing $\sigma$ on $D$-spokes is
+equivalent to the existence of $(o_0, \dots, o_{m-1}) \in \{0,1\}^m$
+satisfying, for each $j$:
+\begin{itemize}
+  \item if $L_j = 1$: $R_j(o_j) = L_{j+1}(o_{j+1})$ (an equality
+        clause);
+  \item if $L_j = 2$: $R_j(o_j) \neq L_{j+1}(o_{j+1})$ (an inequality
+        clause);
+  \item if $L_j \geq 3$: no constraint.
+\end{itemize}
+Each clause is a 2-CNF clause on the variables $o_j, o_{j+1}$, so
+the system is a cyclic 2-SAT.
+\end{prop}
+
+\begin{proof}
+Cycle edges within a gap depend only on $R_j$ and $L_{j+1}$ (by
+Lemma~\ref{lem:gap}), which depend only on $(o_j, o_{j+1})$.
+The proper-coloring constraints at the $U$-positions and $D$-positions
+not at the boundary of the gap are taken care of by gap feasibility.
+\end{proof}
+
+\subsection*{The remaining step}
+
+\begin{conj}[2-SAT solvability]
+\label{conj:2sat}
+For every $\sigma \in \mathcal{P}_m$ with $m \in \{4, 6\}$ and the
+balanced triangulation with $m_1 \geq m - 1$, the cyclic 2-SAT
+system of Proposition~\ref{prop:reduction} is satisfiable.
+\end{conj}
+
+\textbf{Empirical verification.}  For $m = 6$, $m_1 \in \{5, \dots,
+8\}$ all $36$ elements of $\mathcal{P}_6$ admit between $6$ and $18$
+satisfying orientation assignments (script:
+\texttt{experiments/orbit\_decomposition.py}).  No counterexample
+exists in the tested range.
+
+\textbf{Why a clean general proof is non-trivial.}
+The straightforward attempt --- ``$o_j = 0$ for all $j$ is always
+satisfying'' --- fails:  the rainbow $\sigma = (1, 2, 3, 2, 3, 1)$
+at $m_1 = 6$ has $R_4(0) = L_5(0) = 2$, violating the $L_4 = 2$ clause.
+A satisfying assignment exists (e.g.\ $(0, 0, 0, 0, 1, 0)$) but the
+needed flip depends on $\sigma$.  A correct general proof must
+analyse the implication graph of the cyclic 2-SAT, which has
+$\sigma$-dependent forbidden combinations.
+
+The forbidden $(o_j, o_{j+1})$ combo at a length-$2$ gap depends on
+the pair $(\sigma_j, \sigma_{j+1})$ via the third color
+$u := \{1,2,3\} \setminus \{\sigma_j, \sigma_{j+1}\}$:
+\begin{center}
+\begin{tabular}{lll}
+\toprule
+case & forbidden $(o_j, o_{j+1})$ & implication\\
+\midrule
+$\sigma_j = \sigma_{j+1}$ & $(0,1), (1,0)$ & $o_j = o_{j+1}$\\
+$\sigma_j, \sigma_{j+1} \in \{2,3\}$, $u = 1$ & $(1, 0)$ & $o_j = 1 \Rightarrow o_{j+1} = 1$\\
+$(\sigma_j, \sigma_{j+1}) = (1, 3)$, $u = 2$ & $(1, 1)$ & $o_j = 1 \Rightarrow o_{j+1} = 0$\\
+$(\sigma_j, \sigma_{j+1}) = (3, 1)$, $u = 2$ & $(0, 0)$ & $o_j = 0 \Rightarrow o_{j+1} = 1$\\
+$\sigma_j, \sigma_{j+1} \in \{1,2\}$, $u = 3$ & $(0, 1)$ & $o_j = 0 \Rightarrow o_{j+1} = 0$\\
+\bottomrule
+\end{tabular}
+\end{center}
+
+A clean proof of Conjecture~\ref{conj:2sat} likely proceeds by:
+(i) Showing the implication graph on $\{(o_j, o_{j+1})\}$ is bipartite
+in a strong sense that prevents the cyclic chain from forcing a
+contradiction;  (ii) Reducing modulo color symmetry ($S_3$ acts on
+$\sigma$ and on the orientation labels jointly), since
+$\mathcal{P}_m$ has $|\mathcal{P}_m| / 6 = 6$ orbits and verifying
+solvability on $6$ representatives suffices.
+
+\section*{The sharpness counterexample}
+
+\begin{prop}[Sharpness at $m_1 = m - 2$]
+\label{prop:sharpness}
+At $m = 6, m_1 = 4$, the rainbow $\sigma = (1, 2, 3, 2, 3, 1)$ is
+\emph{not} in $\pi_D$.
+\end{prop}
+
+\begin{proof}
+Balanced triangulation gives two length-$1$ gaps, between
+$D$-positions $(2,3)$ (with $(\sigma_1, \sigma_2) = (2, 3)$,
+forcing $c(e_2) = 1$) and $(7,8)$ (with $(\sigma_4, \sigma_5) =
+(3, 1)$, forcing $c(e_7) = 2$).  Propagating through
+$T'_{\mathrm{ann}}$ via the remaining length-$2$ gaps:
+$c(e_3) = 2$ (from $D$-position $3$), $c(e_8) = 3$ (from $D$-position
+$8$), $c(e_9) = 2$ (from $U$-position $9$ with $c(e_8) = 3$),
+$c(e_0) = 3$ (from $D$-position $0$), $c(e_1) = 1$ (from $U$-position
+$1$ with $c(e_0) = 3$), but the constraint at $D$-position $2$ then
+demands $c(e_1) = 3 \neq 1$.  Contradiction.
+\end{proof}
+
+\section*{What this gives us}
+
+Combining Lemma~\ref{lem:o-face}, Proposition~\ref{prop:reduction},
+and the (empirically verified, not proven)
+Conjecture~\ref{conj:2sat}:
+
+\begin{cor}[Provisional]
+\label{cor:provisional}
+For $m \in \{4, 6\}$ and balanced triangulation with $m_1 \geq m - 1$:
+$\pi_D = \mathcal{P}_m$, in particular the rainbow $S_3$-orbit lies
+in $\pi_D$.
+\end{cor}
+
+\begin{cor}[Chain pigeonhole simplification, conditional]
+\label{cor:chain}
+Conditional on Conjecture~\ref{conj:2sat}, the chain-pigeonhole step
+at $|\gamma| = m$ for an antipodal-chord SP tire $T_1$ with $m_1
+\geq m - 1$ reduces to:  $\pi_U(\mathcal{C}(T_2)) \cap \mathcal{P}_m
+\neq \emptyset$, i.e.\ a non-empty intersection on the perms-per-half
+set rather than on all of $\{1,2,3\}^m$.
+\end{cor}
+
+\section*{What's missing}
+
+A clean structural proof of Conjecture~\ref{conj:2sat}.  Two
+candidate routes:
+\begin{enumerate}
+  \item \textbf{$S_3$-equivariant case analysis.}  Reduce to $6$
+        representative $\sigma$'s (one per $S_3$-orbit) and explicitly
+        construct a satisfying $o$ for each at $m_1 = m - 1$ (the
+        tightest case).
+  \item \textbf{Global implication-graph analysis.}  Show that the
+        cyclic chain of implications never produces a contradiction.
+        This likely involves a parity argument on the number of
+        ``odd implications'' around the cycle.
+\end{enumerate}
+
+\end{document}