coloring_nested_tire_graphs: rigorous proof of cut tire forest proposition (high-side refinement)
Replaces the informal Stage 2 argument with a rigorous one,
achieved by refining the proposition to high-side faces only.
KEY INSIGHT: the original (unrestricted) proposition was problematic
because the LOW-SIDE face of H_{d+1} (= face containing pendants)
also contains all depth ≤ d edges in its interior, including H_d
edges. Hence low-side H_{d+1} faces span multiple H_d faces.
The fix: restrict to HIGH-SIDE faces only.
For a high-side face f' of H_{d+1}: by Lemma 2 (level-set), f''s
interior contains only depth-> d+1 edges = depth ≥ d+2. Since
depth-d edges are NOT in this range, no H_d edge sits inside f'.
Therefore f' is contained in a unique H_d face (by partition).
This H_d face is also high-side (contains f', which contains
depth-≥d+2 edges, hence depth->d).
Result: high-side cut tires form a forest, rigorously. The proof
uses only Lemma 1 (BFS-adj) and Lemma 2 (level-set), no rotation
system case analysis needed.
Low-side cut tires are not relevant for chain pigeonhole; the
single low-side face is identified with the cut C itself as the
forest's "virtual root."
Note grows to 5 pages.
Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com>
This commit is contained in:
@@ -2,6 +2,6 @@
|
||||
\newlabel{prop:tree}{{}{1}}
|
||||
\newlabel{lem:bfs-adj}{{}{1}}
|
||||
\newlabel{lem:level-set}{{}{1}}
|
||||
\@writefile{toc}{\contentsline {paragraph}{Caveat on Stage 2.}{2}{}\protected@file@percent }
|
||||
\@writefile{toc}{\contentsline {paragraph}{Remark on the proof.}{2}{}\protected@file@percent }
|
||||
\@writefile{toc}{\contentsline {paragraph}{Reformulated chain half (tree DP form).}{5}{}\protected@file@percent }
|
||||
\gdef \@abspage@last{5}
|
||||
|
||||
@@ -1,4 +1,4 @@
|
||||
This is pdfTeX, Version 3.141592653-2.6-1.40.24 (TeX Live 2022) (preloaded format=pdflatex 2022.10.5) 26 MAY 2026 22:24
|
||||
This is pdfTeX, Version 3.141592653-2.6-1.40.24 (TeX Live 2022) (preloaded format=pdflatex 2022.10.5) 26 MAY 2026 22:32
|
||||
entering extended mode
|
||||
restricted \write18 enabled.
|
||||
%&-line parsing enabled.
|
||||
@@ -178,20 +178,20 @@ File: l3backend-pdftex.def 2022-02-07 L3 backend support: PDF output (pdfTeX)
|
||||
(./cut_tire_tree_structure.aux)
|
||||
\openout1 = `cut_tire_tree_structure.aux'.
|
||||
|
||||
LaTeX Font Info: Checking defaults for OML/cmm/m/it on input line 15.
|
||||
LaTeX Font Info: ... okay on input line 15.
|
||||
LaTeX Font Info: Checking defaults for OMS/cmsy/m/n on input line 15.
|
||||
LaTeX Font Info: ... okay on input line 15.
|
||||
LaTeX Font Info: Checking defaults for OT1/cmr/m/n on input line 15.
|
||||
LaTeX Font Info: ... okay on input line 15.
|
||||
LaTeX Font Info: Checking defaults for T1/cmr/m/n on input line 15.
|
||||
LaTeX Font Info: ... okay on input line 15.
|
||||
LaTeX Font Info: Checking defaults for TS1/cmr/m/n on input line 15.
|
||||
LaTeX Font Info: ... okay on input line 15.
|
||||
LaTeX Font Info: Checking defaults for OMX/cmex/m/n on input line 15.
|
||||
LaTeX Font Info: ... okay on input line 15.
|
||||
LaTeX Font Info: Checking defaults for U/cmr/m/n on input line 15.
|
||||
LaTeX Font Info: ... okay on input line 15.
|
||||
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).]
|
||||
@@ -249,81 +249,28 @@ e
|
||||
* \@reversemarginfalse
|
||||
* (1in=72.27pt=25.4mm, 1cm=28.453pt)
|
||||
|
||||
LaTeX Font Info: Trying to load font information for U+msa on input line 16.
|
||||
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 16.
|
||||
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
|
||||
)
|
||||
) [1
|
||||
|
||||
! LaTeX Error: Environment lem undefined.
|
||||
|
||||
See the LaTeX manual or LaTeX Companion for explanation.
|
||||
Type H <return> for immediate help.
|
||||
...
|
||||
|
||||
l.41 \begin{lem}
|
||||
[BFS depth differs by at most 1 between adjacent edges]
|
||||
Your command was ignored.
|
||||
Type I <command> <return> to replace it with another command,
|
||||
or <return> to continue without it.
|
||||
|
||||
|
||||
! LaTeX Error: \begin{proof} on input line 35 ended by \end{lem}.
|
||||
|
||||
See the LaTeX manual or LaTeX Companion for explanation.
|
||||
Type H <return> for immediate help.
|
||||
...
|
||||
|
||||
l.46 \end{lem}
|
||||
|
||||
Your command was ignored.
|
||||
Type I <command> <return> to replace it with another command,
|
||||
or <return> to continue without it.
|
||||
|
||||
|
||||
! LaTeX Error: Environment lem undefined.
|
||||
|
||||
See the LaTeX manual or LaTeX Companion for explanation.
|
||||
Type H <return> for immediate help.
|
||||
...
|
||||
|
||||
l.57 \begin{lem}
|
||||
[Level-set property of $H_d$]
|
||||
Your command was ignored.
|
||||
Type I <command> <return> to replace it with another command,
|
||||
or <return> to continue without it.
|
||||
|
||||
|
||||
! LaTeX Error: \begin{proof} on input line 35 ended by \end{lem}.
|
||||
|
||||
See the LaTeX manual or LaTeX Companion for explanation.
|
||||
Type H <return> for immediate help.
|
||||
...
|
||||
|
||||
l.67 \end{lem}
|
||||
|
||||
Your command was ignored.
|
||||
Type I <command> <return> to replace it with another command,
|
||||
or <return> to continue without it.
|
||||
|
||||
[1
|
||||
|
||||
{/usr/local/texlive/2022/texmf-var/fonts/map/pdftex/updmap/pdftex.map}]
|
||||
Overfull \hbox (83.47609pt too wide) in paragraph at lines 175--179
|
||||
{/usr/local/texlive/2022/texmf-var/fonts/map/pdftex/updmap/pdftex.map}] [2]
|
||||
Overfull \hbox (83.47609pt too wide) in paragraph at lines 185--189
|
||||
[]\OT1/cmr/m/n/10.95 Compatibility with each child $\OML/cmm/m/it/10.95 T[]$ \O
|
||||
T1/cmr/m/n/10.95 via the bi-jec-tion $\OMS/cmsy/m/n/10.95 f[]\OML/cmm/m/it/10.9
|
||||
5 T[]\OMS/cmsy/m/n/10.95 g $ f[]\OML/cmm/m/it/10.95 T[]\OMS/cmsy/m/n/10.95 g$\O
|
||||
T1/cmr/m/n/10.95 .
|
||||
[]
|
||||
|
||||
[2]
|
||||
Overfull \hbox (0.17146pt too wide) in paragraph at lines 196--198
|
||||
|
||||
Overfull \hbox (0.17146pt too wide) in paragraph at lines 206--208
|
||||
\OT1/cmr/m/n/10.95 Run on $7$ test graphs (script: \OT1/cmtt/m/n/10.95 tree[]st
|
||||
ructure[]sweep.py\OT1/cmr/m/n/10.95 ; data: \OT1/cmtt/m/n/10.95 tree[]structure
|
||||
[]sweep[]data.txt\OT1/cmr/m/n/10.95 ):
|
||||
@@ -331,13 +278,13 @@ ructure[]sweep.py\OT1/cmr/m/n/10.95 ; data: \OT1/cmtt/m/n/10.95 tree[]structure
|
||||
|
||||
[3] [4] [5] (./cut_tire_tree_structure.aux) )
|
||||
Here is how much of TeX's memory you used:
|
||||
3256 strings out of 478268
|
||||
48520 string characters out of 5846347
|
||||
352585 words of memory out of 5000000
|
||||
21443 multiletter control sequences out of 15000+600000
|
||||
3257 strings out of 478268
|
||||
48523 string characters out of 5846347
|
||||
351600 words of memory out of 5000000
|
||||
21444 multiletter control sequences out of 15000+600000
|
||||
479833 words of font info for 69 fonts, out of 8000000 for 9000
|
||||
1141 hyphenation exceptions out of 8191
|
||||
55i,7n,62p,240b,242s stack positions out of 10000i,1000n,20000p,200000b,200000s
|
||||
55i,7n,62p,240b,243s stack positions out of 10000i,1000n,20000p,200000b,200000s
|
||||
{/usr/local/texlive/2022/texmf-dis
|
||||
t/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/
|
||||
@@ -357,7 +304,7 @@ msfonts/cm/cmti10.pfb></usr/local/texlive/2022/texmf-dist/fonts/type1/public/am
|
||||
sfonts/cm/cmtt10.pfb></usr/local/texlive/2022/texmf-dist/fonts/type1/public/ams
|
||||
fonts/symbols/msbm10.pfb></usr/local/texlive/2022/texmf-dist/fonts/type1/public
|
||||
/cm-super/sfrm1095.pfb>
|
||||
Output written on cut_tire_tree_structure.pdf (5 pages, 210419 bytes).
|
||||
Output written on cut_tire_tree_structure.pdf (5 pages, 211700 bytes).
|
||||
PDF statistics:
|
||||
106 PDF objects out of 1000 (max. 8388607)
|
||||
64 compressed objects within 1 object stream
|
||||
|
||||
Binary file not shown.
@@ -18,19 +18,37 @@
|
||||
|
||||
\section*{The claim}
|
||||
|
||||
\begin{prop}[Cut tires form a forest]
|
||||
Let $f$ be a face of $H_d$ in the inherited embedding. By the BFS
|
||||
level-set property (Lemma~\ref{lem:level-set} below), the open
|
||||
interior of $f$ contains only edges of $G'_i$ of depth $< d$ or only
|
||||
edges of depth $> d$. We call $f$ a \emph{high-side} face if its
|
||||
interior contains only depth-$>d$ edges, and a \emph{low-side} face
|
||||
otherwise. The low-side face is the unique face of $H_d$ that
|
||||
contains the pendants (depth $0$ edges).
|
||||
|
||||
\begin{prop}[Cut tires form a forest, refined]
|
||||
\label{prop:tree}
|
||||
For each side $i$ of a $6$-edge cut of $G'$, the cut tires of $G'_i$,
|
||||
parameterised by pairs $(d, f)$ with $d \ge 1$ and $f$ a face of
|
||||
$H_d$, form a \emph{forest} under the parent--child relation
|
||||
For each side $i$ of a $6$-edge cut of $G'$, the high-side cut tires
|
||||
of $G'_i$, parameterised by pairs $(d, f)$ with $d \ge 1$ and $f$ a
|
||||
\emph{high-side} face of $H_d$, form a \emph{forest} under the
|
||||
parent--child relation
|
||||
\[
|
||||
\mathrm{parent}\bigl(T_{d+1}^{(f')}\bigr) := T_d^{(f)}
|
||||
\]
|
||||
where $f$ is the unique face of $H_d$ in whose planar interior $f'$
|
||||
lies in the inherited embedding of $G'_i$.
|
||||
where $f$ is the unique high-side face of $H_d$ in whose planar
|
||||
interior $f'$ lies in the inherited embedding of $G'_i$.
|
||||
|
||||
The forest's roots are the cut tires at depth $1$ (one per face of
|
||||
$H_1$); their ``virtual parent'' is the cut $C$ itself.
|
||||
The forest's roots are the high-side cut tires at depth $1$ (one per
|
||||
high-side face of $H_1$); their ``virtual parent'' is the cut $C$
|
||||
itself.
|
||||
|
||||
\emph{Remark.} The restriction to high-side faces is what makes the
|
||||
geometric containment clean. A low-side face of $H_{d+1}$ contains
|
||||
$H_d$ edges in its interior, so the literal ``face-contained-in-face''
|
||||
relation is not well-defined for low-side faces. In the cut-tire
|
||||
framework, only the high-side faces give the ``concentric'' cut
|
||||
tires we care about for chain pigeonhole; the low-side face is the
|
||||
``outside pendant region'' identified with the cut.
|
||||
\end{prop}
|
||||
|
||||
\begin{proof}
|
||||
@@ -93,51 +111,31 @@ interior).
|
||||
\end{proof}
|
||||
|
||||
\medskip
|
||||
\noindent\textbf{Stage 2: faces of $H_{d+1}$ embed in faces of $H_d$.}
|
||||
\noindent\textbf{Stage 2: high-side faces of $H_{d+1}$ embed in
|
||||
high-side faces of $H_d$.}
|
||||
|
||||
Pendants (depth $0$ edges) lie in some specific face of $H_d$; that
|
||||
face is low-side. All other faces of $H_d$ are high-side and
|
||||
contain depth-$> d$ edges, which includes all of $H_{d+1}$'s edges.
|
||||
Let $f'$ be a high-side face of $H_{d+1}$. By definition, every edge
|
||||
of $G'_i$ in the open interior of $f'$ has depth $> d + 1$.
|
||||
|
||||
Let $f'$ be a face of $H_{d+1}$. We claim $f'$ is contained in
|
||||
exactly one face of $H_d$.
|
||||
In particular, no edge of depth $d$ lies in the open interior of
|
||||
$f'$: every depth-$d$ edge of $G'_i$ has depth $d \neq > d+1$, so
|
||||
depth-$d$ edges are not in $f'$'s open interior.
|
||||
|
||||
\emph{Containment in at least one face:} $f'$ is an open connected
|
||||
region of $\mathbb{R}^2 \setminus H_{d+1}$. In particular it is
|
||||
connected. By Lemma~\ref{lem:level-set}, each face of $H_d$ is
|
||||
either entirely low-side or entirely high-side, and the two types
|
||||
are separated topologically by $H_d$. Suppose for contradiction
|
||||
$f'$ intersects two distinct faces $g_1, g_2$ of $H_d$. Then a
|
||||
path in $f'$ from a point in $g_1$ to a point in $g_2$ crosses some
|
||||
edge of $H_d$ (since faces of $H_d$ are separated by $H_d$ edges).
|
||||
But $H_d \subset E(G'_i) \setminus E(H_{d+1})$, so $H_d$ edges are
|
||||
in $\mathbb{R}^2 \setminus E(H_{d+1})$; they could in principle lie
|
||||
within $f'$ \emph{except} that $f'$ is a maximal connected open
|
||||
component of that complement, which already includes the $H_d$
|
||||
edges. This is where the elementary topological argument is
|
||||
subtle: we need the additional constraint that no $H_d$ edge
|
||||
sits strictly inside $f'$.
|
||||
Therefore $f' \cap H_d = \emptyset$ (where $H_d$ is treated as the
|
||||
topological union of its vertices and edges in $|\Pi|$).
|
||||
Equivalently, $f' \subseteq \mathbb{R}^2 \setminus H_d$.
|
||||
|
||||
\emph{No $H_d$ edge sits strictly inside $f'$:} suppose an $H_d$ edge
|
||||
$e$ is strictly inside $f'$. Then $e$'s endpoints are inside $f'$
|
||||
(or on $\partial f'$). An endpoint $v$ of $e$ is also incident to
|
||||
$H_{d+1}$ edges (since $V(H_d) \cap V(H_{d+1})$ contains vertices
|
||||
where depth-$d$ and depth-$(d+1)$ edges meet; in cubic $G'_i$, $v$
|
||||
has $3$ edges with various depths). The $H_{d+1}$ edges incident
|
||||
to $v$ are on $\partial f'$ (the boundary walk of $f'$), so $v \in
|
||||
\partial f'$. Then $e$'s other endpoint $w$ is also on or inside
|
||||
$f'$. But moving from $v$ along $e$ into $w$: this curve segment
|
||||
is inside $f'$ until it reaches $w$. If $w$ is on $\partial f'$,
|
||||
the entire edge $e$ lies on the boundary closure $\overline{f'}$,
|
||||
not strictly inside. If $w$ is strictly inside $f'$, then $w$'s
|
||||
incident edges (including $e$) project into $f'$ in a way that
|
||||
should appear on $\partial f'$ --- but $e$ is not in $H_{d+1}$,
|
||||
contradiction.
|
||||
Since $f'$ is an open connected region (= face of $H_{d+1}$), and
|
||||
$\mathbb{R}^2 \setminus H_d$ partitions into the disjoint open
|
||||
faces of $H_d$, the connected $f'$ is contained in exactly one
|
||||
face of $H_d$. Call this face $f$. Then $f' \subseteq f$.
|
||||
|
||||
\medskip
|
||||
The careful case analysis shows: no $H_d$ edge sits strictly inside
|
||||
$f'$, hence $f'$ is contained in a single face of $H_d$ (the unique
|
||||
face whose interior contains $f'$).
|
||||
Furthermore, $f$ is high-side: it contains $f'$, which contains
|
||||
depth-$\ge d + 2$ edges, which are $> d$ depth. So $f$ is in the
|
||||
``high-side'' classification of Lemma~\ref{lem:level-set}.
|
||||
|
||||
Hence $\mathrm{parent}(T_{d+1}^{(f')}) := T_d^{(f)}$ is well-defined
|
||||
and unique among high-side cut tires.
|
||||
|
||||
\medskip
|
||||
\noindent\textbf{Conclusion: forest structure.}
|
||||
@@ -150,15 +148,26 @@ at the ``cut'' for the depth-$1$ roots' virtual parent). No cycles
|
||||
can form. Hence the parent relation defines a forest. \qed
|
||||
\end{proof}
|
||||
|
||||
\paragraph{Caveat on Stage 2.} The argument that ``no $H_d$ edge sits
|
||||
strictly inside $f'$'' uses an informal topological case analysis on
|
||||
how an $H_d$ edge inside $f'$ would have to interact with $f'$'s
|
||||
boundary. A fully rigorous proof would set up the topological
|
||||
framework more carefully (e.g.\ via the rotation system of the
|
||||
planar embedding, tracing the boundary walk of $f'$ around an
|
||||
``intruder'' $H_d$ edge to show it must already lie in
|
||||
$\partial f'$). Empirically, the conclusion holds across
|
||||
\textbf{$1486$ tested cases, $0$ failures} (see broader sweep below).
|
||||
\paragraph{Remark on the proof.} Stage 2 is now fully rigorous,
|
||||
thanks to the refinement to \emph{high-side} faces of $H_{d+1}$.
|
||||
The key step is: a high-side face of $H_{d+1}$ contains, by
|
||||
definition, only depth-$\ge d + 2$ edges in its interior. Depth-$d$
|
||||
edges (= $H_d$ edges) are not in this depth range, so they cannot
|
||||
sit inside $f'$. No rotation-system case analysis is needed for the
|
||||
high-side case; the level-set lemma does all the work.
|
||||
|
||||
The original (unrestricted) proposition was problematic for the
|
||||
\emph{low-side} face of $H_{d+1}$, which contains the pendants
|
||||
(depth $0$) plus all edges of depth $\le d$ in $G'_i$'s ``outside''
|
||||
region. This low-side face can contain $H_d$ edges in its interior
|
||||
and therefore spans multiple $H_d$ faces. By restricting to
|
||||
high-side faces, this difficulty is avoided.
|
||||
|
||||
For the cut-tire chain pigeonhole framework, only the high-side
|
||||
cut tires are relevant: they form the ``concentric layers'' going
|
||||
inward from the cut. The low-side face is the unique outside face
|
||||
containing the pendants and is identified with the cut $C$ itself
|
||||
(playing the ``virtual root'' role in the forest).
|
||||
|
||||
\section*{Why this matters for the chain half}
|
||||
|
||||
|
||||
Reference in New Issue
Block a user