coloring_nested_tire_graphs: compare 2-SAT vs König-lift approaches to chain pigeonhole

Adds a side-by-side comparison of the two proof attempts now in
the repo:

  Approach 1 (cyclic 2-SAT, in rainbow_proof.tex):
    Proves π_D = P_m (perms-per-half) for one antipodal-chord SP
    tire when m_1 ≥ m - 1.  Open piece: 2-SAT solvability
    (Conjecture 1.5).

  Approach 2 (König lift, in worst_case_proof_sketch.tex):
    Proves |S_1 ∩ S_2| ≥ 6 for two adjacent SP tires sharing γ
    when both chords are on γ.  Open piece: T_2 induces a
    γ-face partition (Conj t2-induces-partition).

Assessment: Approach 2 is more promising because (a) the hard step
is already proven (König's theorem), (b) it proves exactly what we
need (chain-pigeonhole non-emptiness, not the full π_D
characterisation), and (c) it directly explains the empirical
worst-case |S_1 ∩ S_2| = 6 = single S_3-orbit phenomenon.

Approach 1 still has value if we need finer control over π_D's
shape, but for just establishing non-empty overlap Approach 2
suffices.

Both approaches witness the SAME canonical 6-element worst-case
intersection (the rainbow S_3-orbit at γ=6 = the König-lifted
Latin S_3-orbit).

Recommended next move: attack Conj t2-induces-partition.  Write
down the candidate induced γ-partition explicitly, verify it
computationally, then prove inclusion via transfer-matrix / fibre
lifting.

Note: two_approaches_comparison.tex (3 pages).

Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com>
This commit is contained in:
2026-05-26 11:19:39 -04:00
parent 83df771199
commit f0bc82b88d
4 changed files with 579 additions and 0 deletions
@@ -0,0 +1,2 @@
\relax
\gdef \@abspage@last{4}
@@ -0,0 +1,334 @@
This is pdfTeX, Version 3.141592653-2.6-1.40.24 (TeX Live 2022) (preloaded format=pdflatex 2022.10.5) 26 MAY 2026 11:19
entering extended mode
restricted \write18 enabled.
%&-line parsing enabled.
**two_approaches_comparison.tex
(./two_approaches_comparison.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
)
(./two_approaches_comparison.aux)
\openout1 = `two_approaches_comparison.aux'.
LaTeX Font Info: Checking defaults for OML/cmm/m/it on input line 13.
LaTeX Font Info: ... okay on input line 13.
LaTeX Font Info: Checking defaults for OMS/cmsy/m/n on input line 13.
LaTeX Font Info: ... okay on input line 13.
LaTeX Font Info: Checking defaults for OT1/cmr/m/n on input line 13.
LaTeX Font Info: ... okay on input line 13.
LaTeX Font Info: Checking defaults for T1/cmr/m/n on input line 13.
LaTeX Font Info: ... okay on input line 13.
LaTeX Font Info: Checking defaults for TS1/cmr/m/n on input line 13.
LaTeX Font Info: ... okay on input line 13.
LaTeX Font Info: Checking defaults for OMX/cmex/m/n on input line 13.
LaTeX Font Info: ... okay on input line 13.
LaTeX Font Info: Checking defaults for U/cmr/m/n on input line 13.
LaTeX Font Info: ... okay on input line 13.
(/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 14.
(/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 14.
(/usr/local/texlive/2022/texmf-dist/tex/latex/amsfonts/umsb.fd
File: umsb.fd 2013/01/14 v3.01 AMS symbols B
)
LaTeX Font Info: Font shape `OT1/cmtt/bx/n' in size <14.4> not available
(Font) Font shape `OT1/cmtt/m/n' tried instead on input line 34.
[1
{/usr/local/texlive/2022/texmf-var/fonts/map/pdftex/updmap/pdftex.map}]
Underfull \hbox (badness 10000) in paragraph at lines 141--143
[]\OT1/cmr/m/n/10 Custom orientation-bit ma-chin-ery;
[]
Underfull \hbox (badness 4266) in paragraph at lines 141--143
\OT1/cmr/m/n/10 implication-graph anal-y-sis on a cyclic
[]
Overfull \hbox (39.62682pt too wide) in paragraph at lines 127--160
[]
[]
[2]
! Missing $ inserted.
<inserted text>
$
l.171 written down. The remaining open piece (T_
2 induces a
I've inserted a begin-math/end-math symbol since I think
you left one out. Proceed, with fingers crossed.
! Missing $ inserted.
<inserted text>
$
l.172 $\gamma
$-partition) is a geometric/structural claim about how
I've inserted a begin-math/end-math symbol since I think
you left one out. Proceed, with fingers crossed.
[3] [4] (./two_approaches_comparison.aux) )
Here is how much of TeX's memory you used:
3258 strings out of 478268
48612 string characters out of 5846347
350557 words of memory out of 5000000
21443 multiletter control sequences out of 15000+600000
481954 words of font info for 77 fonts, out of 8000000 for 9000
1141 hyphenation exceptions out of 8191
55i,11n,62p,242b,279s 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/f
onts/type1/public/amsfonts/cm/cmbx10.pfb></usr/local/texlive/2022/texmf-dist/fo
nts/type1/public/amsfonts/cm/cmbx12.pfb></usr/local/texlive/2022/texmf-dist/fon
ts/type1/public/amsfonts/cm/cmbxti10.pfb></usr/local/texlive/2022/texmf-dist/fo
nts/type1/public/amsfonts/cm/cmex10.pfb></usr/local/texlive/2022/texmf-dist/fon
ts/type1/public/amsfonts/cm/cmmi10.pfb></usr/local/texlive/2022/texmf-dist/font
s/type1/public/amsfonts/cm/cmmi7.pfb></usr/local/texlive/2022/texmf-dist/fonts/
type1/public/amsfonts/cm/cmmi8.pfb></usr/local/texlive/2022/texmf-dist/fonts/ty
pe1/public/amsfonts/cm/cmr10.pfb></usr/local/texlive/2022/texmf-dist/fonts/type
1/public/amsfonts/cm/cmr12.pfb></usr/local/texlive/2022/texmf-dist/fonts/type1/
public/amsfonts/cm/cmr17.pfb></usr/local/texlive/2022/texmf-dist/fonts/type1/pu
blic/amsfonts/cm/cmr7.pfb></usr/local/texlive/2022/texmf-dist/fonts/type1/publi
c/amsfonts/cm/cmr8.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/cm/cmtt10.pfb></usr/local/texlive/2022/texmf-dist/fonts/type1/public/amsfon
ts/cm/cmtt12.pfb></usr/local/texlive/2022/texmf-dist/fonts/type1/public/cm-supe
r/sfrm1095.pfb>
Output written on two_approaches_comparison.pdf (4 pages, 214518 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,243 @@
\documentclass[11pt]{article}
\usepackage{amsmath,amssymb,amsthm}
\usepackage{graphicx}
\usepackage{geometry}
\usepackage{booktabs}
\geometry{margin=1in}
\title{Two approaches to the chain-pigeonhole step:\\
cyclic 2-SAT vs.\ K\"onig lift}
\author{}
\date{}
\begin{document}
\maketitle
\section*{Background}
The chain-pigeonhole step asks whether, for any adjacent SP tire pair
$(T_1, T_2)$ sharing cycle $\gamma$ of length $k$, the
projection-supports overlap non-trivially:
\[
\pi_D(\mathcal{C}(T_1)) \cap \pi_U(\mathcal{C}(T_2)) \ne \emptyset.
\]
Empirically (\texttt{tire\_fiber\_step2.tex} +
\texttt{tire\_fiber\_step2\_large.tex}) the overlap is always
non-empty, and in the worst case has exactly $6$ elements forming a
single $S_3$-orbit.
Two independent proof attempts now exist in the notes, attacking
slightly different statements with very different techniques. This
note compares them and assesses which is more promising.
\section*{Approach 1: cyclic 2-SAT
(\texttt{rainbow\_proof.tex})}
\subsection*{What it tries to prove}
A single-tire characterisation: for an antipodal-chord SP tire $T$
with $m_1 \ge m - 1$,
\[
\pi_D(\mathcal{C}(T)) \;=\; \mathcal{P}_m,
\]
where $\mathcal{P}_m \subseteq \{1,2,3\}^m$ is the
``perms-per-face'' set ($(m/2)!^2 \cdot \binom{3}{m/2}^2 = 36$
elements at both $m \in \{4, 6\}$).
\subsection*{Technique}
\begin{enumerate}
\item \textbf{$\subseteq$ direction:} clean from the
$O$-face dual proper-colouring constraint.
\item \textbf{Reduce $\supseteq$ to 2-SAT:} For each
$\sigma \in \mathcal{P}_m$, define orientation bits
$o_0, \dots, o_{m-1} \in \{0,1\}$ at the $D$-positions.
The proper-colouring constraint on $T'_{\mathrm{ann}}$
becomes a cyclic 2-SAT on these orientations.
\item \textbf{Open step (Conjecture 1.5):} the cyclic 2-SAT is
satisfiable for every $\sigma \in \mathcal{P}_m$.
Empirically true ($6$--$18$ satisfying orientations per
$\sigma$ at $m = 6$), but a clean structural proof is open.
\end{enumerate}
\subsection*{Status}
The $\subseteq$ direction is fully proven. The $\supseteq$ direction
reduces to a 2-SAT solvability claim that remains open as
Conjecture~1.5; a naive ``all-zero orientation'' construction fails,
and a correct general argument needs implication-graph or
$S_3$-equivariant case analysis.
\section*{Approach 2: K\"onig lift
(\texttt{worst\_case\_proof\_sketch.tex})}
\subsection*{What it tries to prove}
A two-tire overlap statement: for adjacent SP tires $(T_1, T_2)$
sharing $\gamma$ with both sides above their saturation thresholds,
\[
|\pi_D(\mathcal{C}(T_1)) \cap \pi_U(\mathcal{C}(T_2))| \;\ge\; 6.
\]
This is the actual chain-pigeonhole question (no need to characterise
$\pi_D$ as a whole).
\subsection*{Technique}
\begin{enumerate}
\item \textbf{Build a bipartite face-incidence graph $G$:} left
vertices $=$ $T_1$'s $\gamma$-face partition $\mathcal{F}_1$;
right vertices $=$ $T_2$'s $\gamma$-face partition
$\mathcal{F}_2$; edges $=$ $\gamma$-edges (each lies in one
$\mathcal{F}_1$-face and one $\mathcal{F}_2$-face). Each
face has exactly $3$ $\gamma$-edges, so $G$ is $3$-regular
bipartite.
\item \textbf{Apply K\"onig's theorem:} every bipartite graph admits
a proper $\Delta$-edge-colouring. $G$ gets a proper
$3$-edge-colouring $\chi : E(G) \to \{1, 2, 3\}$.
\item \textbf{Lift back to $\gamma$:} define $\sigma(e) := \chi(e)$
for each $\gamma$-edge. Then at every $\mathcal{F}_1$-face
(and $\mathcal{F}_2$-face), the three incident edges have
three distinct colours, so $\sigma|_F$ is a permutation of
$\{1,2,3\}$.
\item Hence $\sigma$ lies in the Latin overlap, and its $S_3$
orbit (size $6$) is in $\pi_D \cap \pi_U$.
\end{enumerate}
\subsection*{What's still open}
The construction works directly when \emph{both} tires give a chord
on $\gamma$ (so both $\mathcal{F}_1, \mathcal{F}_2$ are direct
$\gamma$-face partitions). In the actual chain-pigeonhole setup,
$T_2$'s chord is on $B_{\mathrm{in}}^{(2)}$, not on $\gamma$.
\textbf{Open conjecture
(Conj.\ \emph{t2-induces-partition} of the worst-case note):} $T_2$
nonetheless induces a $\gamma$-face partition
$\widetilde{\mathcal{F}_2}$ such that $\pi_U(\mathcal{C}(T_2))
\supseteq \mathcal{L}(\gamma, \widetilde{\mathcal{F}_2})$ (the Latin
subset of $\gamma$-colourings compatible with
$\widetilde{\mathcal{F}_2}$). A candidate construction exists:
group $\gamma$-edges by which $B_{\mathrm{in}}^{(2)}$-face their
$T_2$-side annular triangles share an edge with.
\section*{Side-by-side comparison}
\begin{center}
\small
\begin{tabular}{l|p{0.4\textwidth}|p{0.4\textwidth}}
\toprule
& \textbf{Approach 1: cyclic 2-SAT} & \textbf{Approach 2: K\"onig lift}\\
\midrule
What it proves
& Single-tire: $\pi_D = \mathcal{P}_m$ (a full structural
characterisation, $|\pi_D| = 36$).
& Two-tire: $|S_1 \cap S_2| \ge 6$ (a lower bound on the
overlap, witnessed by the rainbow $S_3$-orbit).\\
Hard step
& Cyclic 2-SAT solvability for every $\sigma \in \mathcal{P}_m$.
& Showing $T_2$'s side induces a $\gamma$-face partition when
$T_2$'s chord is on $B_{\mathrm{in}}^{(2)}$ rather than $\gamma$.\\
Tooling
& Custom orientation-bit machinery; implication-graph
analysis on a cyclic 2-SAT.
& Classical: K\"onig's edge-colouring theorem for bipartite
graphs.\\
Strength of conclusion
& Stronger than needed: characterises $\pi_D$ exactly.
& Exactly what's needed for chain pigeonhole.\\
What's proven
& $\subseteq$ direction (Lemma 1.2); 2-SAT reduction (Prop 1.4);
sharpness counterexample (Prop 1.7).
& K\"onig-overlap prop (when both chords on $\gamma$);
$S_3$-invariance lower-bound argument.\\
What's open
& 2-SAT solvability (Conj 1.5); empirically verified.
& ``$T_2$ induces $\gamma$-partition'' (Conj
\emph{t2-induces-partition}); plausibility check via candidate
construction.\\
\bottomrule
\end{tabular}
\end{center}
\section*{Which approach is more promising}
\textbf{Approach 2 (K\"onig lift) is more promising}, for three
reasons:
\subsection*{1.\ The hard step is already proven}
K\"onig's theorem is a 100-year-old textbook result. The K\"onig-
overlap proposition is a clean lift via that theorem and is fully
written down. The remaining open piece (T_2 induces a
$\gamma$-partition) is a geometric/structural claim about how
$T_2$'s annular triangulation distributes $B_{\mathrm{in}}^{(2)}$ faces
across $\gamma$-edges --- likely amenable to a direct construction.
Approach 1's open piece (2-SAT solvability) is a combinatorial
satisfiability claim with no obvious leveraged tool. Empirically
true, but the structural reason isn't yet clear.
\subsection*{2.\ Approach 2 proves exactly what we want}
Chain pigeonhole asks: is the overlap non-empty? Approach 2 directly
addresses this with a lower bound of $6$, which is also empirically
tight. Approach 1 proves a strictly stronger statement (the full
$\pi_D = \mathcal{P}_m$ characterisation) that is more than chain
pigeonhole needs. Proving more than necessary is a strictly harder
task and unnecessary for the goal.
\subsection*{3.\ The K\"onig lower bound has the right structure}
Worst-case overlap is empirically a single $S_3$-orbit of size $6$,
which is exactly what the K\"onig lift produces (lift one
3-edge-colouring, then act by $S_3$ on colours). The proof
mirror the empirical phenomenon. Approach 1's machinery is more
general and doesn't naturally explain why the worst case is an
$S_3$-orbit.
\subsection*{When Approach 1 still pays off}
Approach 1 \emph{does} give a stronger result: a complete
characterisation of $\pi_D$ for the antipodal-chord SP tire,
including the upper bound $|\pi_D| \le 36$. This is useful if we
ever need finer control over $\pi_D$'s shape (e.g.\ if we want to
prove that $\pi_D$ does not contain certain $S_3$-orbits, or if we
want to control the chain-pigeonhole overlap above the floor of
$6$). For just establishing non-empty overlap, Approach 2 suffices.
\section*{Reconciliation: the $6$ is the same $6$}
Both approaches witness the same canonical $6$-element worst-case
intersection:
\begin{itemize}
\item Approach 1: the rainbow $S_3$-orbit $(a, b, c, b, c, a) \cdot
S_3$ sits inside $\pi_D \cap \pi_U$ when $\pi_D = \mathcal{P}_m$
contains it and $\pi_U$ does too.
\item Approach 2: the K\"onig-lifted Latin colouring's $S_3$-orbit
sits inside the intersection directly, by construction.
\end{itemize}
For the case $T_1$ antipodal-chord SP, $T_2$ chordless SR, $k = 6$
(the worst tested case), these are literally the same $6$ elements.
\section*{Recommended next move}
Attack the open conjecture in Approach 2 (Conj
\emph{t2-induces-partition}):
\begin{enumerate}
\item Write down the candidate induced $\gamma$-partition
$\widetilde{\mathcal{F}_2}$ explicitly (the
``group $\gamma$-edges by which
$B_{\mathrm{in}}^{(2)}$-face's neighbours they share
annular edges with'' construction).
\item Verify $\pi_U(\mathcal{C}(T_2)) \supseteq
\mathcal{L}(\gamma, \widetilde{\mathcal{F}_2})$ computationally
for $k \in \{3, 4, 5, 6\}$ and several $T_2$ structures.
\item If empirical fit is exact (as in the worst-case data),
prove inclusion via a transfer-matrix / fibre-lifting
argument.
\end{enumerate}
This is more leveraged than continuing to refine the 2-SAT
implication-graph analysis, which would prove a stronger statement
that we do not need.
\end{document}