coloring_nested_tire_graphs: add note explaining 2-SAT solvability

Standalone explanation of what "2-SAT solvability" means in the
context of the rainbow proof (rainbow_proof.tex, Conjecture 1.5):

- Defines 2-SAT in general (boolean variables, 2-variable clauses,
  P-time decidable).
- Maps it onto our rainbow proof: variables = orientation bits o_j
  at D-positions; clauses = inter-D-position gap constraints; cyclic
  chain wraps around T'_ann.
- "Solvable" ⇔ proper edge 3-coloring with given σ exists, i.e.
  σ ∈ π_D.
- Cyclic 2-SAT can in principle fail; toy example (3-cycle of
  not-equal clauses = odd-cycle 2-coloring obstruction).
- Empirically our system never fails for σ ∈ P_m (6-18 satisfying
  orientations per σ at m=6), but a structural proof is open.
- Why it matters: proving Conjecture 1.5 upgrades the rainbow
  proof's provisional corollary into a theorem and reduces chain
  pigeonhole to the perms-per-half overlap.

Note: two_sat_solvability.tex (3 pages).

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

papers/coloring_nested_tire_graphs/notes/two_sat_solvability.aux

@@ -0,0 +1,2 @@
+\relax 
+\gdef \@abspage@last{2}

papers/coloring_nested_tire_graphs/notes/two_sat_solvability.log

@@ -0,0 +1,300 @@
+This is pdfTeX, Version 3.141592653-2.6-1.40.24 (TeX Live 2022) (preloaded format=pdflatex 2022.10.5)  26 MAY 2026 11:12
+entering extended mode
+ restricted \write18 enabled.
+ %&-line parsing enabled.
+**two_sat_solvability.tex
+(./two_sat_solvability.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 two_sat_solvability.aux.
+\openout1 = `two_sat_solvability.aux'.
+
+LaTeX Font Info:    Checking defaults for OML/cmm/m/it on input line 12.
+LaTeX Font Info:    ... okay on input line 12.
+LaTeX Font Info:    Checking defaults for OMS/cmsy/m/n on input line 12.
+LaTeX Font Info:    ... okay on input line 12.
+LaTeX Font Info:    Checking defaults for OT1/cmr/m/n on input line 12.
+LaTeX Font Info:    ... okay on input line 12.
+LaTeX Font Info:    Checking defaults for T1/cmr/m/n on input line 12.
+LaTeX Font Info:    ... okay on input line 12.
+LaTeX Font Info:    Checking defaults for TS1/cmr/m/n on input line 12.
+LaTeX Font Info:    ... okay on input line 12.
+LaTeX Font Info:    Checking defaults for OMX/cmex/m/n on input line 12.
+LaTeX Font Info:    ... okay on input line 12.
+LaTeX Font Info:    Checking defaults for U/cmr/m/n on input line 12.
+LaTeX Font Info:    ... okay on input line 12.
+(/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 13.
+
+(/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 13.
+
+
+(/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}]
+Overfull \hbox (58.79611pt too wide) in paragraph at lines 123--127
+\OT1/cmr/m/n/10.95 tem al-ways has be-tween $6$ and $18$ sat-is-fy-ing as-sign-
+ments (com-puted in \OT1/cmtt/m/n/10.95 experiments/orbit[]decomposition.py\OT1
+/cmr/m/n/10.95 ). 
+ []
+
+[2] (./two_sat_solvability.aux) ) 
+Here is how much of TeX's memory you used:
+ 3232 strings out of 478268
+ 48192 string characters out of 5846347
+ 349533 words of memory out of 5000000
+ 21423 multiletter control sequences out of 15000+600000
+ 477519 words of font info for 59 fonts, out of 8000000 for 9000
+ 1141 hyphenation exceptions out of 8191
+ 55i,8n,62p,236b,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/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/p
+ublic/amsfonts/cm/cmmi10.pfb></usr/local/texlive/2022/texmf-dist/fonts/type1/pu
+blic/amsfonts/cm/cmmi8.pfb></usr/local/texlive/2022/texmf-dist/fonts/type1/publ
+ic/amsfonts/cm/cmr10.pfb></usr/local/texlive/2022/texmf-dist/fonts/type1/public
+/amsfonts/cm/cmr17.pfb></usr/local/texlive/2022/texmf-dist/fonts/type1/public/a
+msfonts/cm/cmr8.pfb></usr/local/texlive/2022/texmf-dist/fonts/type1/public/amsf
+onts/cm/cmsy10.pfb></usr/local/texlive/2022/texmf-dist/fonts/type1/public/amsfo
+nts/cm/cmsy6.pfb></usr/local/texlive/2022/texmf-dist/fonts/type1/public/amsfont
+s/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/amsfonts/c
+m/cmtt10.pfb></usr/local/texlive/2022/texmf-dist/fonts/type1/public/cm-super/sf
+rm1095.pfb>
+Output written on two_sat_solvability.pdf (2 pages, 159662 bytes).
+PDF statistics:
+ 77 PDF objects out of 1000 (max. 8388607)
+ 46 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/two_sat_solvability.tex

@@ -0,0 +1,151 @@
+\documentclass[11pt]{article}
+\usepackage{amsmath,amssymb,amsthm}
+\usepackage{graphicx}
+\usepackage{geometry}
+\usepackage{booktabs}
+\geometry{margin=1in}
+
+\title{What ``2-SAT solvability'' means in the rainbow proof}
+\author{}
+\date{}
+
+\begin{document}
+\maketitle
+
+\section*{2-SAT in general}
+
+\textbf{2-SAT} is short for \emph{2-satisfiability}.  Standard logical
+problem:
+\begin{itemize}
+  \item You have a set of \emph{boolean variables}
+        $x_1, x_2, \dots, x_n$, each taking value $0$ or $1$
+        (false/true).
+  \item You have a set of \emph{clauses}, each a constraint involving
+        exactly \emph{two} variables.
+  \item \textbf{2-SAT solvability} $=$ ``does there exist an
+        assignment of $0/1$ to all variables such that every clause
+        is satisfied simultaneously?''
+\end{itemize}
+
+2-SAT is polynomial-time decidable (linear time, in fact) using the
+\emph{implication graph} and \emph{strongly-connected components}.
+This is in contrast to 3-SAT (3 variables per clause), which is
+NP-complete.
+
+\section*{In our setup (the rainbow proof)}
+
+\textbf{Variables.}  $o_0, o_1, \dots, o_{m-1} \in \{0, 1\}$, one
+\emph{orientation bit} per $D$-position on the dual annular cycle
+$T'_{\mathrm{ann}}$.  At each $D$-position $p_j$, the two incident
+cycle edges must take the two colors of $\{1, 2, 3\} \setminus
+\{\sigma_j\}$ in some order; $o_j$ decides which color sits on the
+left of $p_j$ versus the right.
+
+\textbf{Clauses.}  One per inter-$D$-position gap on
+$T'_{\mathrm{ann}}$.  Each gap involves two adjacent orientations
+$(o_j, o_{j+1})$ and forbids certain combinations:
+
+\begin{center}
+\begin{tabular}{lll}
+\toprule
+gap type & clause type & combos forbidden \\
+\midrule
+length-$1$, $\sigma_j \ne \sigma_{j+1}$
+  & equality (fixed pair)
+  & 3 of 4 forbidden, leaves one valid combo \\
+length-$1$, $\sigma_j = \sigma_{j+1}$
+  & $o_j = o_{j+1}$
+  & $(0,1)$ and $(1,0)$ forbidden \\
+length-$2$, $\sigma_j \ne \sigma_{j+1}$
+  & one combo forbidden
+  & 1 of 4 forbidden \\
+length-$2$, $\sigma_j = \sigma_{j+1}$
+  & $o_j = o_{j+1}$
+  & $(0,1)$ and $(1,0)$ forbidden \\
+length-$\ge 3$
+  & no clause
+  & gap has full slack \\
+\bottomrule
+\end{tabular}
+\end{center}
+
+Each clause involves exactly two variables, so the system is 2-SAT.
+
+\textbf{Cyclic structure.}  Because the gaps wrap cyclically around
+$T'_{\mathrm{ann}}$, the clauses form a \emph{cyclic} chain ---
+clause on $(o_0, o_1)$, then $(o_1, o_2)$, $\ldots$, finally
+$(o_{m-1}, o_0)$.
+
+\section*{What ``solvable'' means concretely}
+
+For a given $\sigma \in \mathcal{P}_m$:
+\begin{itemize}
+  \item \textbf{Solvable} $\Leftrightarrow$ there is an orientation
+        $(o_0, \dots, o_{m-1})$ satisfying all clauses simultaneously
+        $\Rightarrow$ proper edge $3$-coloring of $T'_{f'}$ inducing
+        $\sigma$ exists $\Rightarrow$ $\sigma \in \pi_D$.
+  \item \textbf{Unsolvable} $\Leftrightarrow$ no such orientation
+        $\Rightarrow$ $\sigma \notin \pi_D$.
+\end{itemize}
+
+So the rainbow proof's \textbf{Conjecture~1.5 (2-SAT solvability)}
+says: for every $\sigma$ with both halves a permutation of
+$\{1, 2, 3\}$, the resulting cyclic 2-SAT system has at least one
+satisfying assignment.
+
+\section*{Why a cyclic 2-SAT chain can fail}
+
+A 2-SAT cycle \emph{can} be unsolvable when the implications chain
+around and force a contradiction.  Toy example with 3 variables on
+a cycle:
+\begin{itemize}
+  \item Clause 1: $o_0 \ne o_1$.
+  \item Clause 2: $o_1 \ne o_2$.
+  \item Clause 3: $o_2 \ne o_0$.
+\end{itemize}
+
+Implications:
+\[
+   o_0 = 0 \;\Rightarrow\; o_1 = 1 \;\Rightarrow\; o_2 = 0
+       \;\Rightarrow\; o_0 = 1.
+\]
+Contradiction.  So this $3$-cycle of ``not-equal'' clauses is
+unsatisfiable (it is the chromatic-number obstruction: a triangle
+has no proper $2$-coloring).
+
+\section*{Why we believe our cyclic chain doesn't fail}
+
+For our $m$-variable cyclic 2-SAT (with clauses determined by
+$\sigma \in \mathcal{P}_m$), the analogous question is: does the
+specific pattern of clauses ever create such a wrap-around
+contradiction?
+
+\textbf{Empirically:} no.  For $m = 6$, $m_1 \in \{5, 6, 7, 8\}$ and
+all $36$ elements of $\mathcal{P}_6$, the cyclic 2-SAT system always
+has between $6$ and $18$ satisfying assignments (computed in
+\texttt{experiments/orbit\_decomposition.py}).
+
+\textbf{Structurally:} the constraints have a special form
+(forbidden combos depend on $\sigma_j, \sigma_{j+1}$ via the third
+color $u = \{1, 2, 3\} \setminus \{\sigma_j, \sigma_{j+1}\}$).
+The hope is that a parity or implication-graph argument shows the
+cyclic chain cannot consistently wrap around to a contradiction
+when $\sigma$ has the perms-per-half shape.  This argument is what
+the proof of Conjecture~1.5 would supply, and what is currently
+missing.
+
+\section*{Why we care}
+
+Proving Conjecture~1.5 would convert
+\texttt{rainbow\_proof.tex}'s ``provisional corollary'' into a
+genuine theorem:
+\[
+   \pi_D(\mathcal{C}(T)) = \mathcal{P}_m
+   \quad \text{whenever } m_1 \ge m - 1,
+\]
+which in turn upgrades the chain-pigeonhole step at $|\gamma| = m$
+to a structural claim of the form ``$\pi_U(\mathcal{C}(T_2))$ meets
+the fixed $36$-element set $\mathcal{P}_m$,'' a strictly smaller and
+more tractable overlap condition than ``$\pi_U$ meets $\pi_D$.''
+
+\end{document}