coloring_nested_tire_graphs: broader empirical sweep of loose conjecture (k>=2 form)

Adopts the k>=2 refinement of the loose chain pigeonhole conjecture
(per loose_conjecture_counterexamples.tex) and runs a broader sweep:

  - All 6 Holton-McKay non-Hamiltonian 38-vertex cubic plane graphs.
  - 3 candidate matching 6-edge cuts per graph (greedy search,
    preferring matching cuts then balance).
  - Both sides of each cut.
  - All depths d >= 1.
  - Brute-force enumerate proper edge 3-colorings (skipping cut
    tires with > 14 edges due to runtime).

Results:
  - 287 total cut tires examined.
  - 154 with k >= 2 in/out spokes.
  - 107 verifiable (≤ 14 edges).
  - ALL 107 passed: |π(T)| >= 6 with at least one full S_3-orbit.
  - 0 counterexamples found.

This is strong empirical support for the k>=2 form of the loose
conjecture's per-tire half.

The cut_depth_label note (now 7 pages) is updated with:
  - k >= 2 restriction in the conjecture statement.
  - Restriction rationale (k=1 trivially excluded).
  - Status: empirical sweep + provable spoke-only case.

Files:
  experiments/loose_conjecture_sweep.py
  experiments/loose_conjecture_sweep_data.txt
  notes/cut_depth_label.tex (updated)

Next step: the per-tire half is essentially provable for spoke-only
cut tires via Prop 1.13. The chain half remains the genuinely open
piece.

Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com>
This commit is contained in:
2026-05-26 16:48:54 -04:00
parent 6093b8cce3
commit 902db37b50
5 changed files with 391 additions and 44 deletions
@@ -0,0 +1,207 @@
"""Broader empirical sweep of the (k >= 2) loose chain pigeonhole
conjecture on cut tires.
For each of the 6 Holton-McKay graphs:
- Find multiple 6-edge cuts (preferring matching cuts).
- For each cut, build cut tires on both halves at every depth.
- For each cut tire with total spoke count k >= 2, check whether
|π(T)| >= 6.
Report any cut tire with k >= 2 and |π(T)| < 6 (= counterexample).
"""
import os
import sys
from itertools import permutations, product
from sage.all import Graph
HERE = os.path.dirname(os.path.abspath(__file__))
sys.path.insert(0, HERE)
from cut_depth_label import (
parse_planar_code, HM_FILE, find_six_edge_cut,
apply_procedure, compute_nice_layout,
)
from cut_tire import cut_tire_at
from cut_tire_test import build_cut_tire_graph, enumerate_proper_edge_3colorings
def find_multiple_six_cuts(G, max_cuts=5):
"""Find multiple distinct 6-edge cuts via greedy search from
different starts."""
n = G.order()
candidates_seen = set()
candidates_list = []
for start in G.vertices():
S = {start}
boundary = 3
prev_size = -1
while True:
if boundary == 6 and 2 <= len(S) <= n - 2:
S_fro = frozenset(S)
if S_fro not in candidates_seen:
cut = [(u, v) for u in S for v in G.neighbors(u)
if v not in S]
if len(cut) == 6:
candidates_seen.add(S_fro)
endpoints_in_S = [u for (u, v) in cut if u in S] + \
[v for (u, v) in cut if v in S]
endpoints_in_Sc = [u for (u, v) in cut if u not in S] + \
[v for (u, v) in cut if v not in S]
is_matching = (len(set(endpoints_in_S)) == 6 and
len(set(endpoints_in_Sc)) == 6)
balance = abs(len(S) - n / 2)
candidates_list.append((S_fro, cut, is_matching,
balance))
if len(S) == prev_size:
break
prev_size = len(S)
frontier = []
for w in G.vertices():
if w in S: continue
if any(nb in S for nb in G.neighbors(w)):
edges_into_S = sum(1 for nb in G.neighbors(w) if nb in S)
frontier.append((edges_into_S, w))
if not frontier:
break
frontier.sort(reverse=True)
_, w = frontier[0]
edges_into_S = sum(1 for nb in G.neighbors(w) if nb in S)
S.add(w)
boundary = boundary + 3 - 2 * edges_into_S
if len(S) >= n - 1:
break
# Sort: matching first, then balanced
candidates_list.sort(key=lambda x: (-int(x[2]), x[3]))
return [(S, cut) for (S, cut, _, _) in candidates_list[:max_cuts]]
def quick_projection(tire):
"""Build the cut tire graph and brute-force enumerate proper
edge 3-colorings to compute |π(T)| and orbit decomposition.
Skip if too many edges."""
G_tire, edge_labels, _ = build_cut_tire_graph(tire, 0)
n_edges = G_tire.size()
if n_edges > 14:
return None
edges_norm, colorings = enumerate_proper_edge_3colorings(G_tire)
out_idx = [i for i, e in enumerate(edges_norm) if edge_labels[e] == 'out']
in_idx = [i for i, e in enumerate(edges_norm) if edge_labels[e] == 'in']
proj = set()
for c in colorings:
sigma = (tuple(c[i] for i in out_idx), tuple(c[i] for i in in_idx))
proj.add(sigma)
# Orbit decomposition
seen = set()
orbit_sizes = []
has_full_orbit = False
for sigma in sorted(proj):
if sigma in seen: continue
orbit = set()
for pi in permutations((1, 2, 3)):
mapped = (tuple(pi[c - 1] for c in sigma[0]),
tuple(pi[c - 1] for c in sigma[1]))
orbit.add(mapped)
orbit_in_proj = orbit & proj
orbit_sizes.append(len(orbit_in_proj))
if len(orbit_in_proj) == 6:
has_full_orbit = True
seen |= orbit_in_proj
return {
'n_edges': n_edges,
'n_colorings': len(colorings),
'proj_size': len(proj),
'orbit_sizes': sorted(orbit_sizes),
'has_full_orbit': has_full_orbit,
'k_total': len(out_idx) + len(in_idx),
}
def sweep():
gs = parse_planar_code(HM_FILE)
print(f'Loaded {len(gs)} Holton-McKay graphs\n')
counterexamples = []
n_tires_tested = 0
n_k_ge_2 = 0
n_passed = 0
for hm_idx, G in enumerate(gs):
print(f'=== HM #{hm_idx} ===', flush=True)
try:
cuts = find_multiple_six_cuts(G, max_cuts=3)
except Exception as e:
print(f' cut search failed: {e}')
continue
print(f' Found {len(cuts)} candidate cuts to test', flush=True)
base_pos = compute_nice_layout(G)
for cut_idx, (S, cut) in enumerate(cuts):
S0 = frozenset(S)
S1 = frozenset(G.vertices()) - S0
print(f' Cut #{cut_idx}: |S|={len(S0)}, '
f'matching={len(set(u for (u,v) in cut if u in S0) | set(v for (u,v) in cut if v in S0)) == 6 and len(set(u for (u,v) in cut if u not in S0) | set(v for (u,v) in cut if v not in S0)) == 6}',
flush=True)
for side, S_side in [('0', S0), ('1', S1)]:
if len(S_side) < 4 or len(S_side) > G.order() - 4:
continue
try:
H, pos, ed, _, _, _ = apply_procedure(
G, S_side, cut, base_pos, side,
pendant_start_id=max(G.vertices()) + 1 + (
0 if side == '0' else 50))
except Exception as e:
print(f' side {side}: apply_procedure failed: {e}',
flush=True)
continue
if not ed:
continue
d_max = max(ed.values())
tires_examined_side = 0
tires_passed_side = 0
for d in range(1, d_max + 1):
tires = cut_tire_at(H, ed, d)
for f_idx, tire in enumerate(tires):
k = len(tire['out_spokes']) + len(tire['in_spokes'])
n_tires_tested += 1
tires_examined_side += 1
if k < 2:
continue
n_k_ge_2 += 1
result = quick_projection(tire)
if result is None:
continue
if not result['has_full_orbit']:
counterexamples.append({
'hm': hm_idx, 'cut_idx': cut_idx,
'side': side, 'd': d, 'face': f_idx,
'k': k, 'result': result,
})
print(f' !!! COUNTEREXAMPLE: side {side}, '
f'depth {d}, face {f_idx}: '
f'k={k}, |π|={result["proj_size"]}, '
f'orbits={result["orbit_sizes"]}',
flush=True)
else:
n_passed += 1
tires_passed_side += 1
print(f' side {side}: max_depth={d_max}, '
f'tires={tires_examined_side}, '
f'k>=2 passed={tires_passed_side}',
flush=True)
print(f'\n=== Summary ===')
print(f'Total cut tires examined: {n_tires_tested}')
print(f'Cut tires with k >= 2: {n_k_ge_2}')
print(f'k>=2 tires passing (|π| >= 6 with full S_3 orbit): {n_passed}')
print(f'Counterexamples (k>=2 without full orbit): {len(counterexamples)}')
if counterexamples:
print('\nCounterexample details:')
for ce in counterexamples:
print(f' HM#{ce["hm"]}, cut {ce["cut_idx"]}, side {ce["side"]}, '
f'd={ce["d"]}, face={ce["face"]}, k={ce["k"]}, '
f'|π|={ce["result"]["proj_size"]}, '
f'orbits={ce["result"]["orbit_sizes"]}')
if __name__ == '__main__':
sweep()
@@ -0,0 +1,80 @@
Loaded 6 Holton-McKay graphs
=== HM #0 ===
Found 3 candidate cuts to test
Selected layout: sage-spring (edge-length CV^2 = 0.0515)
Cut #0: |S|=10, matching=True
side 0: max_depth=2, tires=3, k>=2 passed=0
side 1: max_depth=7, tires=13, k>=2 passed=6
Cut #1: |S|=30, matching=True
side 0: max_depth=7, tires=12, k>=2 passed=3
side 1: max_depth=2, tires=3, k>=2 passed=0
Cut #2: |S|=8, matching=True
side 0: max_depth=2, tires=3, k>=2 passed=0
side 1: max_depth=7, tires=11, k>=2 passed=4
=== HM #1 ===
Found 3 candidate cuts to test
Selected layout: sage-spring (edge-length CV^2 = 0.0446)
Cut #0: |S|=10, matching=True
side 0: max_depth=2, tires=3, k>=2 passed=0
side 1: max_depth=6, tires=12, k>=2 passed=7
Cut #1: |S|=30, matching=True
side 0: max_depth=7, tires=14, k>=2 passed=7
side 1: max_depth=2, tires=3, k>=2 passed=0
Cut #2: |S|=8, matching=True
side 0: max_depth=2, tires=3, k>=2 passed=0
side 1: max_depth=7, tires=14, k>=2 passed=7
=== HM #2 ===
Found 3 candidate cuts to test
Selected layout: sage-spring (edge-length CV^2 = 0.0574)
Cut #0: |S|=30, matching=True
side 0: max_depth=6, tires=11, k>=2 passed=4
side 1: max_depth=2, tires=3, k>=2 passed=0
Cut #1: |S|=18, matching=False
side 0: max_depth=4, tires=7, k>=2 passed=2
side 1: max_depth=4, tires=9, k>=2 passed=3
Cut #2: |S|=20, matching=False
side 0: max_depth=4, tires=7, k>=2 passed=2
side 1: max_depth=3, tires=9, k>=2 passed=6
=== HM #3 ===
Found 3 candidate cuts to test
Selected layout: sage-spring (edge-length CV^2 = 0.0505)
Cut #0: |S|=28, matching=True
side 0: max_depth=7, tires=13, k>=2 passed=6
side 1: max_depth=2, tires=3, k>=2 passed=0
Cut #1: |S|=10, matching=True
side 0: max_depth=2, tires=3, k>=2 passed=0
side 1: max_depth=7, tires=13, k>=2 passed=6
Cut #2: |S|=30, matching=True
side 0: max_depth=7, tires=13, k>=2 passed=3
side 1: max_depth=2, tires=3, k>=2 passed=0
=== HM #4 ===
Found 3 candidate cuts to test
Selected layout: sage-spring (edge-length CV^2 = 0.0636)
Cut #0: |S|=30, matching=True
side 0: max_depth=6, tires=13, k>=2 passed=2
side 1: max_depth=2, tires=3, k>=2 passed=0
Cut #1: |S|=20, matching=False
side 0: max_depth=4, tires=6, k>=2 passed=3
side 1: max_depth=3, tires=9, k>=2 passed=7
Cut #2: |S|=20, matching=False
side 0: max_depth=4, tires=9, k>=2 passed=4
side 1: max_depth=4, tires=9, k>=2 passed=3
=== HM #5 ===
Found 3 candidate cuts to test
Selected layout: sage-spring (edge-length CV^2 = 0.0577)
Cut #0: |S|=30, matching=True
side 0: max_depth=5, tires=12, k>=2 passed=6
side 1: max_depth=2, tires=3, k>=2 passed=0
Cut #1: |S|=20, matching=False
side 0: max_depth=4, tires=8, k>=2 passed=2
side 1: max_depth=3, tires=9, k>=2 passed=7
Cut #2: |S|=20, matching=False
side 0: max_depth=4, tires=9, k>=2 passed=4
side 1: max_depth=4, tires=9, k>=2 passed=3
=== Summary ===
Total cut tires examined: 287
Cut tires with k >= 2: 154
k>=2 tires passing (|π| >= 6 with full S_3 orbit): 107
Counterexamples (k>=2 without full orbit): 0
@@ -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 16:15
This is pdfTeX, Version 3.141592653-2.6-1.40.24 (TeX Live 2022) (preloaded format=pdflatex 2022.10.5) 26 MAY 2026 16:48
entering extended mode
restricted \write18 enabled.
%&-line parsing enabled.
@@ -317,29 +317,58 @@ om \OT1/cmtt/m/n/10.95 rainbow[]proof.tex \OT1/cmr/m/n/10.95 and \OT1/cmtt/m/n/
10.95 worst[]case[]proof[]sketch.tex\OT1/cmr/m/n/10.95 )
[]
Runaway argument?
{quote>
! Paragraph ended before \end was complete.
<to be read again>
\par
l.266
I suspect you've forgotten a `}', causing me to apply this
control sequence to too much text. How can we recover?
My plan is to forget the whole thing and hope for the best.
Overfull \hbox (0.56282pt too wide) in paragraph at lines 267--278
\OT1/cmr/bx/n/10.95 Jus-ti-fi-ca-tion of the per-tire half.[] \OT1/cmr/m/n/10.
95 The per-tire half is es-sen-tially Propo-si-tion 1.13 of \OT1/cmtt/m/n/10.95
paper.tex\OT1/cmr/m/n/10.95 :
Overfull \hbox (39.12393pt too wide) in paragraph at lines 267--275
\OT1/cmr/m/n/10.95 never $6$. Such tires triv-ially vi-o-late ``$\OMS/cmsy/m/n/
10.95 j\OML/cmm/m/it/10.95 ^^Y\OT1/cmr/m/n/10.95 (\OML/cmm/m/it/10.95 T\OT1/cmr
/m/n/10.95 )\OMS/cmsy/m/n/10.95 j ^^U \OT1/cmr/m/n/10.95 6$'' (see \OT1/cmtt/m/
n/10.95 loose[]conjecture[]counterexamples.tex\OT1/cmr/m/n/10.95 ,
[]
[3]
Overfull \hbox (115.9405pt too wide) in paragraph at lines 300--307
\OT1/cmr/bx/n/10.95 Sta-tus.[] \OT1/cmr/m/n/10.95 Em-pir-i-cally true for ev-e
ry cut tire in the Holton-McKay #0 ex-am-ple (tested in \OT1/cmtt/m/n/10.95 cut
[]tire[]conjecture[]tests.tex\OT1/cmr/m/n/10.95 ).
Overfull \hbox (37.97836pt too wide) in paragraph at lines 311--315
\OT1/cmr/m/n/10.95 (\OT1/cmtt/m/n/10.95 experiments/loose[]conjecture[]sweep.py
\OT1/cmr/m/n/10.95 ; data: \OT1/cmtt/m/n/10.95 loose[]conjecture[]sweep[]data.t
xt\OT1/cmr/m/n/10.95 ):
[]
Overfull \hbox (46.78696pt too wide) in paragraph at lines 310--317
[4]
Overfull \hbox (101.53708pt too wide) in paragraph at lines 341--348
\OT1/cmr/m/n/10.95 The pro-ce-dure mir-rors the $4$CT cut-and-reglue scheme (\O
T1/cmtt/m/n/10.95 rainbow[]proof.tex\OT1/cmr/m/n/10.95 , \OT1/cmtt/m/n/10.95 wo
rst[]case[]proof[]sketch.tex\OT1/cmr/m/n/10.95 ,
[]
[4] [5] [6 <./fig_cut_depth_label.png>] [7 <./fig_cut_tire.png>]
(./cut_depth_label.aux) )
! LaTeX Error: \begin{quote} on input line 251 ended by \end{document}.
See the LaTeX manual or LaTeX Companion for explanation.
Type H <return> for immediate help.
...
l.381 \end{document}
Your command was ignored.
Type I <command> <return> to replace it with another command,
or <return> to continue without it.
[5] [6 <./fig_cut_depth_label.png>] [7 <./fig_cut_tire.png>]
(./cut_depth_label.aux) )
(\end occurred inside a group at level 1)
### semi simple group (level 1) entered at line 251 (\begingroup)
### bottom level
Here is how much of TeX's memory you used:
4593 strings out of 478268
74520 string characters out of 5846347
@@ -348,23 +377,23 @@ Here is how much of TeX's memory you used:
479342 words of font info for 67 fonts, out of 8000000 for 9000
1141 hyphenation exceptions out of 8191
55i,8n,63p,656b,312s 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/a
msfonts/cm/cmbx12.pfb></usr/local/texlive/2022/texmf-dist/fonts/type1/public/am
sfonts/cm/cmitt10.pfb></usr/local/texlive/2022/texmf-dist/fonts/type1/public/am
sfonts/cm/cmmi10.pfb></usr/local/texlive/2022/texmf-dist/fonts/type1/public/ams
fonts/cm/cmmi8.pfb></usr/local/texlive/2022/texmf-dist/fonts/type1/public/amsfo
nts/cm/cmr10.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/cmr8.pfb></usr/local/texlive/2022/texmf-dist/fonts/type1/public/amsfonts/cm/
cmsy10.pfb></usr/local/texlive/2022/texmf-dist/fonts/type1/public/amsfonts/cm/c
msy8.pfb></usr/local/texlive/2022/texmf-dist/fonts/type1/public/amsfonts/cm/cmt
i10.pfb></usr/local/texlive/2022/texmf-dist/fonts/type1/public/amsfonts/cm/cmtt
10.pfb></usr/local/texlive/2022/texmf-dist/fonts/type1/public/amsfonts/symbols/
msbm10.pfb></usr/local/texlive/2022/texmf-dist/fonts/type1/public/cm-super/sfrm
1095.pfb>
Output written on cut_depth_label.pdf (7 pages, 519218 bytes).
{/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/c
m/cmbx12.pfb></usr/local/texlive/2022/texmf-dist/fonts/type1/public/amsfonts/cm
/cmitt10.pfb></usr/local/texlive/2022/texmf-dist/fonts/type1/public/amsfonts/cm
/cmmi10.pfb></usr/local/texlive/2022/texmf-dist/fonts/type1/public/amsfonts/cm/
cmmi8.pfb></usr/local/texlive/2022/texmf-dist/fonts/type1/public/amsfonts/cm/cm
r10.pfb></usr/local/texlive/2022/texmf-dist/fonts/type1/public/amsfonts/cm/cmr1
7.pfb></usr/local/texlive/2022/texmf-dist/fonts/type1/public/amsfonts/cm/cmr8.p
fb></usr/local/texlive/2022/texmf-dist/fonts/type1/public/amsfonts/cm/cmsy10.pf
b></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.pfb><
/usr/local/texlive/2022/texmf-dist/fonts/type1/public/amsfonts/cm/cmtt10.pfb></
usr/local/texlive/2022/texmf-dist/fonts/type1/public/amsfonts/symbols/msbm10.pf
b></usr/local/texlive/2022/texmf-dist/fonts/type1/public/cm-super/sfrm1095.pfb>
Output written on cut_depth_label.pdf (7 pages, 522399 bytes).
PDF statistics:
104 PDF objects out of 1000 (max. 8388607)
62 compressed objects within 1 object stream
@@ -249,12 +249,12 @@ ones --- one that does not require special face-boundary structure
and may be easier to prove:
\begin{quote}
\textbf{Loose chain pigeonhole conjecture (cut tires).} Let
$T = T_d^{(i, f)}$ be a non-trivial cut tire (one with at least one
in or out spoke). Then the joint projection $\pi(T)$ is non-empty,
$S_3$-closed, and contains at least one full $S_3$-orbit (i.e.\
$|\pi(T)| \geq 6$, with equality only in the degenerate case where
$\pi(T)$ is a single non-constant $S_3$-orbit).
\textbf{Loose chain pigeonhole conjecture (cut tires, $k \ge 2$
form).} Let $T = T_d^{(i, f)}$ be a cut tire with total spoke
count $|\text{in spokes}| + |\text{out spokes}| \ge 2$. Then the
joint projection $\pi(T)$ is non-empty, $S_3$-closed, and contains
at least one full $S_3$-orbit of size $6$ (i.e.\ a $\sigma$ using
$\ge 2$ distinct colours), giving $|\pi(T)| \geq 6$.
Consequently, for the chain $T_1^{(i)} \to T_2^{(i)} \to \cdots$ on
each side of a cut, the realisable cut-configuration set
@@ -262,7 +262,16 @@ $\mathcal{R}_i$ contains a full $S_3$-orbit, and the intersection
$\mathcal{R}_0 \cap \mathcal{R}_1$ contains a common $S_3$-orbit
(of size $6$), forcing $\mathcal{R}_0 \cap \mathcal{R}_1 \ne
\emptyset$.
\end{quote}
\end{quote>
\noindent\emph{Restriction rationale.} Cut tires with exactly $k =
1$ in/out spoke have $\pi(T) \subseteq \{1, 2, 3\}$, where every
single-colour $\sigma$ has $S_3$-stabilizer of order $2$, so its
$S_3$-orbit has size $6 / 2 = 3$, never $6$. Such tires trivially
violate ``$|\pi(T)| \ge 6$''
(see \texttt{loose\_conjecture\_counterexamples.tex}, where two
$k = 1$ cut tires are exhibited in $G'_1$ of Holton-McKay \#0).
The $k \ge 2$ restriction excludes these trivially excluded cases.
\paragraph{Justification of the per-tire half.} The per-tire half
is essentially Proposition~1.13 of \texttt{paper.tex}: a spoke-only
@@ -297,13 +306,35 @@ strict structural claim about the antipodal-chord SP case), nor
the K\"onig-lift conjecture's specific construction; it would only
recover the bottom-line chain pigeonhole result.
\paragraph{Status.} Empirically true for every cut tire in the
Holton-McKay \#0 example (tested in
\texttt{cut\_tire\_conjecture\_tests.tex}). No general proof.
The per-tire half is essentially provable via Prop~1.13 plus
$S_3$-equivariance. The chain half is the genuinely open question
--- it requires showing that the per-tire $S_3$-orbit structure
composes coherently through the depth chain.
\paragraph{Status.} Strong empirical support:
\begin{itemize}
\item Broader sweep across all $6$ Holton-McKay graphs, $3$ cuts
per graph, both sides
(\texttt{experiments/loose\_conjecture\_sweep.py};
data: \texttt{loose\_conjecture\_sweep\_data.txt}):
\begin{itemize}
\item $287$ total cut tires examined.
\item $154$ with $k \ge 2$ in/out spokes.
\item $107$ of these had $\le 14$ edges and were
brute-force verified; the remaining $47$ were too
large to enumerate exhaustively.
\item \textbf{All $107$ passed: $|\pi(T)| \ge 6$ with a
full $S_3$-orbit.}
\item \textbf{$0$ counterexamples found.}
\end{itemize}
\item The per-tire half (existence of a multi-color spoke
configuration) is provable for spoke-only cut tires (face
boundary a simple cycle of length $n \ge 3$) via Prop~1.13:
$2^n + 2(-1)^n$ total proper edge $3$-colourings, of which
at most $6$ are ``all-spokes-same-color''
(only possible when $n$ is even and the cycle admits a
$2$-edge-colouring), leaving $\ge 2^n + 2(-1)^n - 6 > 0$
multi-color configurations for $n \ge 3$ even or $n \ge 3$
odd.
\item The chain half is the genuinely open question --- it requires
showing that the per-tire $S_3$-orbit structure composes
coherently through the depth chain.
\end{itemize}
\section*{Connection to chain pigeonhole / 4CT reducibility}