didericis/math-research
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

coloring_nested_tire_graphs: partial proof of closed-chain non-emptiness identifies the 4CT-equivalent gap

Browse Source 
Attempts to prove item 1 (non-emptiness of state at L_n in closed
SR+PDS chains ending at outer triangle). Results:

PROVEN:
- S_3-closure preserved by chain propagation.
- State at L_n is either empty OR equals all 6 permutations of {1,2,3}
  (the only non-empty S_3-closed subset of permutations).
- Non-emptiness propagates through intermediate tires under outward
  PDS via step-1 saturation.

REMAINING GAP (conjecture, empirically true): state at L_{n-1}
intersects the "perm-paired" subset of T_n's σ_D-projection (the
σ_D values that pair with permutation σ_U). At the final step T_n
has m_n=3 < k_n, so saturation fails — chain state at L_{n-1} could
in principle lie entirely in the (non-perm-paired) parity-matching
σ_D's, but empirically doesn't.

KEY STRUCTURAL FINDING: for T=(3, k), the σ_D's paired with a
permutation σ_U equal exactly the (parity-matching σ_D's) ∩ (T's
σ_D-projection). Verified for k=3..10.

HONEST OBSERVATION: a structural proof of the remaining conjecture
(without invoking 4CT) would constitute a new proof of 4CT under
the SR+PDS modelling assumption. The chain-pigeonhole framework
reduces to this single reachability question.

Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com>
This commit is contained in:
didericis
2026-05-26 12:58:20 -04:00
parent c8ddbb5d9f
commit 1513922dec
4 changed files with 598 additions and 0 deletions
Download Patch File Download Diff File Expand all files Collapse all files
papers/coloring_nested_tire_graphs/notes/nonemptiness_partial_proof.aux
+8
View File
@@ -0,0 +1,8 @@
\relax
\newlabel{lem:s3-closure}{{1}{1}}
\newlabel{thm:six-or-zero}{{1}{1}}
\newlabel{lem:saturation-nonempty}{{2}{1}}
\newlabel{cor:open-nonempty}{{3}{2}}
\@writefile{toc}{\contentsline {paragraph}{Key observation.}{2}{}\protected@file@percent }
\newlabel{conj:perm-reach}{{}{2}}
\gdef \@abspage@last{3}
papers/coloring_nested_tire_graphs/notes/nonemptiness_partial_proof.log
+376
View File
@@ -0,0 +1,376 @@
This is pdfTeX, Version 3.141592653-2.6-1.40.24 (TeX Live 2022) (preloaded format=pdflatex 2022.10.5) 26 MAY 2026 12:58
entering extended mode
restricted \write18 enabled.
%&-line parsing enabled.
**nonemptiness_partial_proof.tex
(./nonemptiness_partial_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
)
\c@lemma=\count274
\c@theorem=\count275
(/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=\box52
)
(./nonemptiness_partial_proof.aux)
\openout1 = `nonemptiness_partial_proof.aux'.
LaTeX Font Info: Checking defaults for OML/cmm/m/it on input line 16.
LaTeX Font Info: ... okay on input line 16.
LaTeX Font Info: Checking defaults for OMS/cmsy/m/n on input line 16.
LaTeX Font Info: ... okay on input line 16.
LaTeX Font Info: Checking defaults for OT1/cmr/m/n on input line 16.
LaTeX Font Info: ... okay on input line 16.
LaTeX Font Info: Checking defaults for T1/cmr/m/n on input line 16.
LaTeX Font Info: ... okay on input line 16.
LaTeX Font Info: Checking defaults for TS1/cmr/m/n on input line 16.
LaTeX Font Info: ... okay on input line 16.
LaTeX Font Info: Checking defaults for OMX/cmex/m/n on input line 16.
LaTeX Font Info: ... okay on input line 16.
LaTeX Font Info: Checking defaults for U/cmr/m/n on input line 16.
LaTeX Font Info: ... okay on input line 16.
(/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=\dimen158
\scratchbox=\box53
\nofMPsegments=\count278
\nofMParguments=\count279
\everyMPshowfont=\toks29
\MPscratchCnt=\count280
\MPscratchDim=\dimen159
\MPnumerator=\count281
\makeMPintoPDFobject=\count282
\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 17.
(/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 17.
(/usr/local/texlive/2022/texmf-dist/tex/latex/amsfonts/umsb.fd
File: umsb.fd 2013/01/14 v3.01 AMS symbols B
)
Overfull \hbox (2.4628pt too wide) in paragraph at lines 21--27
\OT1/cmr/m/n/10.95 In \OT1/cmtt/m/n/10.95 absorption[]proof.tex \OT1/cmr/m/n/10
.95 we proved (via the $\OML/cmm/m/it/10.95 K[]$\OT1/cmr/m/n/10.95 -walk par-it
y in-vari-ant) that the forward-propagated
[]
Overfull \hbox (3.4848pt too wide) in paragraph at lines 83--93
\OT1/cmr/m/n/10.95 projection of $^^E[]$ equals all of $\OMS/cmsy/m/n/10.95 f\O
T1/cmr/m/n/10.95 1\OML/cmm/m/it/10.95 ; \OT1/cmr/m/n/10.95 2\OML/cmm/m/it/10.95
; \OT1/cmr/m/n/10.95 3\OMS/cmsy/m/n/10.95 g[]$\OT1/cmr/m/n/10.95 . Hence $[](\
OML/cmm/m/it/10.95 L[]\OT1/cmr/m/n/10.95 ) \OMS/cmsy/m/n/10.95 ^^R f\OT1/cmr/m/
n/10.95 1\OML/cmm/m/it/10.95 ; \OT1/cmr/m/n/10.95 2\OML/cmm/m/it/10.95 ; \OT1/c
mr/m/n/10.95 3\OMS/cmsy/m/n/10.95 g[] \OT1/cmr/m/n/10.95 = \OML/cmm/m/it/10.95
^^[[][]T[]$\OT1/cmr/m/n/10.95 ,
[]
[1
{/usr/local/texlive/2022/texmf-var/fonts/map/pdftex/updmap/pdftex.map}]
! LaTeX Error: Unicode character σ (U+03C3)
not set up for use with LaTeX.
See the LaTeX manual or LaTeX Companion for explanation.
Type H <return> for immediate help.
...
l.103 $\text{state}(L_1)$ equals the σ
-set from proper edge $3$-colourings
You may provide a definition with
\DeclareUnicodeCharacter
! LaTeX Error: Unicode character σ (U+03C3)
not set up for use with LaTeX.
See the LaTeX manual or LaTeX Companion for explanation.
Type H <return> for immediate help.
...
l.115 σ
$_D$-projection is a proper subset of $\{1,2,3\}^{k_n}$. Concretely:
You may provide a definition with
\DeclareUnicodeCharacter
! Undefined control sequence.
l.120 \toprule
The control sequence at the end of the top line
of your error message was never \def'ed. If you have
misspelled it (e.g., `\hobx'), type `I' and the correct
spelling (e.g., `I\hbox'). Otherwise just continue,
and I'll forget about whatever was undefined.
! Undefined control sequence.
<recently read> \midrule
l.122 \midrule
The control sequence at the end of the top line
of your error message was never \def'ed. If you have
misspelled it (e.g., `\hobx'), type `I' and the correct
spelling (e.g., `I\hbox'). Otherwise just continue,
and I'll forget about whatever was undefined.
! Undefined control sequence.
<recently read> \bottomrule
l.127 \bottomrule
The control sequence at the end of the top line
of your error message was never \def'ed. If you have
misspelled it (e.g., `\hobx'), type `I' and the correct
spelling (e.g., `I\hbox'). Otherwise just continue,
and I'll forget about whatever was undefined.
! LaTeX Error: Unicode character σ (U+03C3)
not set up for use with LaTeX.
See the LaTeX manual or LaTeX Companion for explanation.
Type H <return> for immediate help.
...
l.177 ... but doesn't characterise \emph{which} σ
values are in the state.
You may provide a definition with
\DeclareUnicodeCharacter
[2]
Overfull \hbox (4.61479pt too wide) in paragraph at lines 201--204
[]\OT1/cmr/bx/n/10.95 Proven: \OT1/cmr/m/n/10.95 non-emptiness prop-a-gates thr
ough all in-ter-me-di-ate tires un-der out-ward PDS (Cor. 3[]).
[]
[3] (./nonemptiness_partial_proof.aux) )
Here is how much of TeX's memory you used:
3210 strings out of 478268
47563 string characters out of 5846347
351987 words of memory out of 5000000
21398 multiletter control sequences out of 15000+600000
482094 words of font info for 77 fonts, out of 8000000 for 9000
1141 hyphenation exceptions out of 8191
55i,10n,62p,243b,218s stack positions out of 10000i,1000n,20000p,200000b,200000s
{/usr/local/texlive/2022/texmf-dist/fon
ts/enc/dvips/cm-super/cm-super-ts1.enc}</usr/local/texlive/2022/texmf-dist/font
s/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/cmmi10.pfb></usr/local/texlive/2022/texmf-dist/fonts/t
ype1/public/amsfonts/cm/cmmi12.pfb></usr/local/texlive/2022/texmf-dist/fonts/ty
pe1/public/amsfonts/cm/cmmi5.pfb></usr/local/texlive/2022/texmf-dist/fonts/type
1/public/amsfonts/cm/cmmi6.pfb></usr/local/texlive/2022/texmf-dist/fonts/type1/
public/amsfonts/cm/cmmi7.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/cmr6.pfb></usr/local/texlive/2022/texmf-dist/fonts/type1/public/amsf
onts/cm/cmr8.pfb></usr/local/texlive/2022/texmf-dist/fonts/type1/public/amsfont
s/cm/cmsy10.pfb></usr/local/texlive/2022/texmf-dist/fonts/type1/public/amsfonts
/cm/cmsy8.pfb></usr/local/texlive/2022/texmf-dist/fonts/type1/public/amsfonts/c
m/cmti10.pfb></usr/local/texlive/2022/texmf-dist/fonts/type1/public/amsfonts/cm
/cmtt10.pfb></usr/local/texlive/2022/texmf-dist/fonts/type1/public/cm-super/sfr
m1095.pfb>
Output written on nonemptiness_partial_proof.pdf (3 pages, 201148 bytes).
PDF statistics:
100 PDF objects out of 1000 (max. 8388607)
60 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/nonemptiness_partial_proof.pdf
BIN
View File
Binary file not shown.
papers/coloring_nested_tire_graphs/notes/nonemptiness_partial_proof.tex
+214
View File
@@ -0,0 +1,214 @@
\documentclass[11pt]{article}
\usepackage{amsmath,amssymb,amsthm}
\usepackage{graphicx}
\usepackage{geometry}
\geometry{margin=1in}
\title{Closed-chain non-emptiness: a partial proof and the remaining gap}
\author{}
\date{}
\newtheorem{lemma}{Lemma}
\newtheorem{theorem}{Theorem}
\newtheorem{corollary}[lemma]{Corollary}
\newtheorem*{conj}{Conjecture}
\begin{document}
\maketitle
\section*{What this note records}
In \texttt{absorption\_proof.tex} we proved (via the $K_3$-walk parity
invariant) that the forward-propagated state at $L_n$ of a closed
SR + PDS chain ending at the outer triangle is contained in the $6$
permutations of $\{1, 2, 3\}$. This note attempts to prove the
remaining ``non-emptiness'' half: that the state is non-empty (and
hence, by $S_3$ invariance, equals all $6$).
\textbf{Result so far:} the proof closes \emph{conditionally} on a
specific structural property of $T_n$ that holds empirically but I
have not proven in general.
\section*{What's easy}
\begin{lemma}[$S_3$-closure preserved by chain propagation]
\label{lem:s3-closure}
For any SR chain $T_1 | \dots | T_n$ starting from a degenerate-inner
$T_1$, the forward-propagated state at every $L_i$ is closed under
the $S_3$ action on colours.
\end{lemma}
\begin{proof}
Each tire's joint support $\Pi_{T_i}$ is determined by the proper
edge $3$-colourings of $T_i$'s annular dual cycle. The $S_3$ action
on the three colour labels acts uniformly on $C_{n_i}$-colourings,
so $\Pi_{T_i}$ is closed under the diagonal $S_3$ action. Forward
propagation $\text{state}_{i+1} = \{ \sigma_U : \exists \sigma_D \in
\text{state}_i, (\sigma_U, \sigma_D) \in \Pi_{T_{i+1}}\}$ commutes
with $S_3$: if $\sigma$ is in $\text{state}_{i+1}$ via some
$\sigma_D \in \text{state}_i$, then $g \cdot \sigma$ is in
$\text{state}_{i+1}$ via $g \cdot \sigma_D \in \text{state}_i$
(using $S_3$-closure of $\text{state}_i$ inductively).
\end{proof}
\begin{theorem}[Conditional non-emptiness $\Rightarrow$ exactly 6]
\label{thm:six-or-zero}
The forward-propagated state at $L_n$ is either empty, or equals all
$6$ permutations of $\{1, 2, 3\}$.
\end{theorem}
\begin{proof}
By the parity invariant (proved in
\texttt{absorption\_proof.tex}), $\text{state}(L_n) \subseteq$
permutations of $\{1,2,3\}$. The $6$ permutations form a single
$S_3$-orbit (the $S_3$ action on length-$3$ tuples with $3$ distinct
colours is transitive). By Lem.~\ref{lem:s3-closure},
$\text{state}(L_n)$ is $S_3$-closed. An $S_3$-closed subset of a
single $S_3$-orbit is either empty or the whole orbit.
\end{proof}
So non-emptiness $\Leftrightarrow$ state $= 6$ permutations.
\section*{Non-emptiness for intermediate steps}
\begin{lemma}[Saturation preserves non-emptiness in the outward
direction]
\label{lem:saturation-nonempty}
If $T_{i+1}$ has $m_{i+1} \geq k_{i+1}$ (the outward-PDS condition),
then $\text{state}(L_{i+1})$ is non-empty whenever $\text{state}(L_i)$
is non-empty.
\end{lemma}
\begin{proof}
By the spread-projection saturation theorem from step 1, when $m_{i+1}
\geq k_{i+1}$ the $\sigma_D$-projection of $\Pi_{T_{i+1}}$ equals all of
$\{1, 2, 3\}^{k_{i+1}}$. Hence
$\text{state}(L_i) \subseteq \{1,2,3\}^{k_{i+1}} = \sigma_D
\text{-projection of } T_{i+1}$, so every $\sigma_D \in
\text{state}(L_i)$ is in some pair of $\Pi_{T_{i+1}}$. Thus
$\text{state}(L_{i+1}) \ni \sigma_U$ for at least one $\sigma_U$
paired with some $\sigma_D$ in the state. Since
$\text{state}(L_i) \neq \emptyset$, $\text{state}(L_{i+1}) \neq
\emptyset$.
\end{proof}
\begin{corollary}[Open-chain non-emptiness]
\label{cor:open-nonempty}
For any prefix $T_1 | T_2 | \dots | T_j$ of an outward-PDS chain with
$T_1$ degenerate-inner and each subsequent $T_{i+1}$ satisfying
$m_{i+1} \geq k_{i+1}$, the state at $L_j$ is non-empty.
\end{corollary}
\begin{proof}
$\text{state}(L_1)$ equals the σ-set from proper edge $3$-colourings
of $C_{m_1}$, which has $2^{m_1} + 2(-1)^{m_1} > 0$ elements for
$m_1 \geq 3$. Iterate Lem.~\ref{lem:saturation-nonempty}.
\end{proof}
\section*{The remaining piece: the final step at $T_n$}
The final step $T_n$ has $m_n = 3$ (outer triangle). Since $|L_{n-1}|
= k_n \geq 3$ in any non-trivial PDS, typically $k_n \geq 3 = m_n$
and the inequality is reversed.
When $m_n < k_n$ the saturation theorem fails: $T_n$'s
σ$_D$-projection is a proper subset of $\{1,2,3\}^{k_n}$. Concretely:
\begin{center}
\small
\begin{tabular}{c r r r r}
\toprule
$k$ & $|\Pi_{T_n}|$ & $|\sigma_D\text{-proj}|$ & $|\text{parity set}|$ & $|\sigma_D \cap \text{parity}|$ \\
\midrule
3 & 63 & 27 & 6 & 6 \\
5 & 255 & 171 & 60 & 42 \\
6 & 510 & 384 & 183 & 90 \\
9 & 4095 & 3681 & 4920 & 840 \\
\bottomrule
\end{tabular}
\end{center}
\paragraph{Key observation.}
Computationally, the set of $\sigma_D$'s in $T_n$'s
$\sigma_D$-projection that are \emph{also} parity-matching equals
exactly the set of $\sigma_D$'s that pair with a permutation $\sigma_U$
under $\Pi_{T_n}$. Call this set the ``perm-paired'' subset.
For non-emptiness at $L_n$ we need: \textbf{$\text{state}(L_{n-1})$
intersects the perm-paired subset of $T_n$}.
\section*{Restatement of the remaining gap}
\begin{conj}[Perm-paired reachability]
\label{conj:perm-reach}
For any SR + outward-PDS chain $T_1 | \dots | T_{n-1}$ with $T_1$
degenerate-inner, the forward-propagated state at $L_{n-1}$ contains
at least one $\sigma_D$ that is in the perm-paired subset of $T_n =
(3, k_n)$ (i.e., a $\sigma_D$ such that $(\sigma_U, \sigma_D) \in
\Pi_{T_n}$ for some permutation $\sigma_U$).
\end{conj}
This is the only remaining gap. Empirically Conj.~\ref{conj:perm-reach}
holds in every tested chain; theoretically I do not yet have a proof.
\subsection*{What I know about Conj.~\ref{conj:perm-reach}}
\begin{enumerate}
\item By the parity invariant, $\text{state}(L_{n-1}) \subseteq$
parity-matching set on $L_{n-1}$ (size 60 at $k = 5$).
\item The perm-paired subset has size $\leq |\text{parity-matching}|$
and is generally strictly smaller (at $k = 5$, $42 < 60$).
\item Both are $S_3$-closed; both are unions of $S_3$-orbits of size $6$
(no constant orbits, since constants violate parity).
\item Empirically, at sufficiently late stages, $\text{state}(L_{n-1})
= $ full parity-matching set. Since the perm-paired subset is
strictly contained in the parity-matching set, the intersection
is the perm-paired subset itself (non-empty).
\item A clean proof of Conj.~\ref{conj:perm-reach} would seem to
require either (a) showing chain state always equals the full
parity-matching set at $L_{n-1}$, or (b) an explicit
construction of a perm-paired $\sigma_D$ reachable through any
outward-PDS chain.
\end{enumerate}
\subsection*{Why it's not immediate from saturation}
Lem.~\ref{lem:saturation-nonempty} preserves \emph{some} non-empty
state, but doesn't characterise \emph{which} σ values are in the state.
A more refined statement is needed: state at each $L_i$ equals the
full parity-matching set (or at least a strictly-larger-than-empty
subset of perm-paired$_{T_n}$).
\subsection*{Why a Tait+4CT reduction is circular}
In general, ``state at $L_n$ non-empty'' is equivalent to the chain's
underlying cubic planar graph $G'$ admitting a proper edge
$3$-colouring, which by Tait's theorem is equivalent to $G$ being
$4$-colourable. So Conj.~\ref{conj:perm-reach} for arbitrary
outward-PDS chains under SR is essentially the 4CT itself (or rather,
4CT restricted to graphs admitting SR + outward-PDS decompositions).
This means Conj.~\ref{conj:perm-reach} cannot be proven by invoking
4CT --- but a \emph{structural} proof of it, independent of 4CT,
\emph{would constitute} a new proof of 4CT (under the SR + PDS
modelling assumption).
\section*{Summary}
\begin{itemize}
\item \textbf{Proven:} state at $L_n$ is either empty or equals
all 6 permutations of $\{1,2,3\}$ (Thm.~\ref{thm:six-or-zero}).
\item \textbf{Proven:} non-emptiness propagates through all
intermediate tires under outward PDS
(Cor.~\ref{cor:open-nonempty}).
\item \textbf{Conjectured (Conj.~\ref{conj:perm-reach}):}
non-emptiness propagates through the final tire $T_n$.
Empirically true; structural proof would imply 4CT.
\end{itemize}
The clean conclusion: \textbf{the chain-pigeonhole story under SR + PDS
reduces to one specific reachability conjecture about chain states
hitting the perm-paired subset of the final tire}. This is the
sharpest version of the 4CT obstruction in our framework.
\end{document}