Move tire coloring transfer to restrictions paper

This commit is contained in:
2026-06-08 15:09:58 -04:00
parent c27ad69024
commit 6400fdfc5e
36 changed files with 372 additions and 336 deletions
@@ -0,0 +1,103 @@
"""Test the tire inner-boundary three-colour conjecture
(Conjecture 1.31, conj:tire-inner-boundary-three-colour) on the six
duals of the non-Hamiltonian 38-vertex cubic plane graphs found by
Holton & McKay.
Each Holton-McKay graph G' is a 3-connected cubic plane graph on 38
vertices; its planar dual G is a 21-vertex triangulation. We run the
exists-source, vertex-rooted inner-boundary check on each dual.
Run with:
sage -python experiments/check_inner_boundary_on_holton_mckay.py
"""
from __future__ import annotations
import os
import sys
from typing import cast
from sage.all import Graph # type: ignore[attr-defined] # pylint: disable=no-name-in-module
HERE = os.path.dirname(os.path.abspath(__file__))
sys.path.insert(0, HERE)
from check_level_cycle_three_color import ( # noqa: E402
level_sources,
test_graph,
)
HM_FILE = (
"/Users/didericis/Code/math-research/papers/"
"even_level_graph_generators/experiments/nonham38m4.pc"
)
def parse_planar_code_to_sage(path: str) -> list[Graph]:
"""Parse McKay's planar_code file -> list of Sage Graphs."""
with open(path, "rb") as f:
data = f.read()
header = b">>planar_code<<"
assert data.startswith(header), data[:20]
pos = len(header)
out: list[Graph] = []
while pos < len(data):
n = data[pos]
pos += 1
edges = set()
for v in range(n):
while True:
w = data[pos]
pos += 1
if w == 0:
break
edges.add(frozenset((v, w - 1)))
g = Graph([tuple(e) for e in edges], multiedges=False, loops=False)
g.is_planar(set_embedding=True)
out.append(g)
return out
def main() -> int:
hm = parse_planar_code_to_sage(HM_FILE)
print(f"Loaded {len(hm)} Holton-McKay graphs from {HM_FILE}\n")
all_pass = True
for i, gprime in enumerate(hm, start=1):
# Dual: triangulation of the sphere. Sage's planar_dual requires a
# plane embedding; gprime already has one set above.
dual = cast(Graph, gprime.planar_dual())
n = dual.order()
e = dual.size()
print(f"=== HM #{i}: G' has {gprime.order()} vertices, "
f"{gprime.size()} edges; dual has n={n}, m={e} ===")
# Sanity: triangulation has 3n - 6 edges.
if e != 3 * n - 6:
print(f" WARNING: dual is not a triangulation (m != 3n-6)")
sources = list(level_sources(dual, "vertex", None))
passed, complete, checked = test_graph(
dual,
sources,
max_colorings=None,
stop_first=True,
quantifier="exists-source",
restriction="inner-boundary",
)
status = "PASS" if (passed and complete) else (
"UNKNOWN" if not complete else "FAIL"
)
print(f" {status}: sources_tried={checked}/{len(sources)}\n")
if not (passed and complete):
all_pass = False
print("---")
print(
"All Holton-McKay duals satisfy the inner-boundary conjecture: "
f"{all_pass}"
)
return 0 if all_pass else 1
if __name__ == "__main__":
raise SystemExit(main())
@@ -0,0 +1,445 @@
"""Empirical test for the level-cycle three-colour conjecture and its
tire inner-boundary refinement.
The level-cycle conjecture (``--restriction level-cycle``, the default)
says: for every maximal planar graph G, there is some level source S and
some proper 4-vertex-colouring c such that every simple cycle contained
in a single level G[L_d] uses at most three colours.
The inner-boundary conjecture (``--restriction inner-boundary``) is the
weakening that constrains only the inner boundaries B_in of the tires in
a tire-tree decomposition rooted at a vertex source: for every G there is
a vertex source v0 and a proper 4-colouring c such that every tire inner
boundary uses at most three colours. Because the inner outerplanar graph
O of a depth-d tire satisfies O = G[component faces] cap L_{d+1} and is
outerplanar, V(B_in) is exactly the level-(d+1) vertices of the tire's
dual component (see the inner-boundary remark in the paper).
Important: both checks are cycle-by-cycle. Two cycles in the same level
or the same inner outerplanar component may omit different colours.
Run examples:
sage -python experiments/check_level_cycle_three_color.py 4 9
sage -python experiments/check_level_cycle_three_color.py 4 8 --quantifier all-sources
sage -python experiments/check_level_cycle_three_color.py 4 8 --sources all
sage -python experiments/check_level_cycle_three_color.py 4 9 --restriction inner-boundary
"""
from __future__ import annotations
import argparse
from collections import defaultdict, deque
from itertools import combinations
from typing import Any, Iterable, Iterator, Sequence, cast
from sage.all import Graph, graphs # type: ignore[attr-defined] # pylint: disable=no-name-in-module
from sage.graphs.graph_coloring import all_graph_colorings # type: ignore[attr-defined] # pylint: disable=no-name-in-module
Coloring = dict[Any, int]
Source = tuple[Any, ...]
def vertex_key(v: Any) -> str:
"""Stable ordering key for Sage vertex labels."""
return repr(v)
def is_induced_cycle(g: Graph, vertices: Sequence[Any]) -> bool:
"""Return True iff G[vertices] is a simple cycle."""
if len(vertices) < 3:
return False
h = cast(Graph, g.subgraph(list(vertices)))
return h.is_connected() and h.num_edges() == len(vertices) and all(
h.degree(v) == 2 for v in h.vertices()
)
def induced_cycle_sources(g: Graph, max_size: int | None = None) -> Iterator[Source]:
"""Yield every vertex set inducing a simple cycle in G."""
vertices = sorted(g.vertices(), key=vertex_key)
upper = len(vertices) if max_size is None else min(max_size, len(vertices))
for k in range(3, upper + 1):
for subset in combinations(vertices, k):
if is_induced_cycle(g, subset):
yield tuple(subset)
def level_sources(g: Graph, mode: str, max_cycle_source_size: int | None) -> Iterator[Source]:
"""Yield level sources according to the requested mode."""
if mode in ("vertex", "all"):
for v in sorted(g.vertices(), key=vertex_key):
yield (v,)
if mode in ("cycle", "all"):
yield from induced_cycle_sources(g, max_cycle_source_size)
def distances_from_source(g: Graph, source: Source) -> dict[Any, int]:
"""Shortest-path distance from a vertex or cycle source."""
if len(source) == 1:
return dict(g.shortest_path_lengths(source[0]))
distances = {v: 0 for v in source}
queue: deque[Any] = deque(source)
while queue:
v = queue.popleft()
for w in g.neighbor_iterator(v):
if w in distances:
continue
distances[w] = distances[v] + 1
queue.append(w)
return distances
def simple_cycle_vertex_sets(g: Graph) -> set[frozenset[Any]]:
"""Enumerate vertex sets of simple cycles in an undirected graph.
The DFS only starts a cycle at its least vertex under vertex_key, which
avoids most duplicates; the final frozenset de-duplicates cycles with the
same vertex set.
"""
vertices = sorted(g.vertices(), key=vertex_key)
index = {v: i for i, v in enumerate(vertices)}
cycles: set[frozenset[Any]] = set()
def dfs(start: Any, current: Any, path: list[Any], seen: set[Any]) -> None:
for nxt in g.neighbor_iterator(current):
if nxt == start:
if len(path) >= 3:
cycles.add(frozenset(path))
continue
if nxt in seen:
continue
if index[nxt] <= index[start]:
continue
seen.add(nxt)
path.append(nxt)
dfs(start, nxt, path, seen)
path.pop()
seen.remove(nxt)
for start in vertices:
dfs(start, start, [start], {start})
return cycles
def level_cycle_violation(
g: Graph, distances: dict[Any, int], coloring: Coloring
) -> tuple[int, frozenset[Any], set[int]] | None:
"""Return the first level cycle using all four colours, if any."""
by_level: dict[int, list[Any]] = {}
for v, d in distances.items():
by_level.setdefault(d, []).append(v)
for d in sorted(by_level):
if len(by_level[d]) < 3:
continue
h = cast(Graph, g.subgraph(by_level[d]))
for cycle in simple_cycle_vertex_sets(h):
used = {coloring[v] for v in cycle}
if len(used) > 3:
return d, cycle, used
return None
def inner_boundary_vertex_sets(g: Graph, source: Source) -> list[frozenset[Any]]:
"""Inner-boundary vertex sets of the tire-tree decomposition at a vertex.
The tire-tree decomposition is defined only for a single-vertex source
placed on the outer face. Each tire is a connected component of the
depth-d dual subgraph G'_d (faces whose minimum vertex level is d). Because
a depth-d face has its three vertex levels in {d, d+1} (adjacent vertices
differ by at most one level), and because the inner outerplanar graph O of
the tire is outerplanar (so every vertex of O lies on its inner-boundary
walk), the inner-boundary vertex set equals the level-(d+1) vertices of the
component: V(B_in) = V(O) = V(component) cap L_{d+1}.
We work on the sphere dual (all faces). The choice of outer face does not
change any inner-boundary set: depth->=1 components are untouched by removing
a depth-0 face, and the root tire always has O = G[L_1].
Only sets of size >= 4 are returned; smaller sets can never use four colours.
"""
if len(source) != 1:
raise ValueError("inner-boundary restriction requires a vertex source")
distances = distances_from_source(g, source)
emb = cast(Graph, g.copy())
if not emb.is_planar(set_embedding=True):
raise ValueError("graph is not planar; cannot build tire decomposition")
faces = emb.faces()
face_vertices: list[set[Any]] = []
for face in faces:
verts: set[Any] = set()
for edge in face:
verts.add(edge[0])
verts.add(edge[1])
face_vertices.append(verts)
depths = [min(distances[v] for v in verts) for verts in face_vertices]
edge_faces: dict[frozenset[Any], list[int]] = defaultdict(list)
for i, face in enumerate(faces):
for edge in face:
edge_faces[frozenset((edge[0], edge[1]))].append(i)
dual_adj: dict[int, set[int]] = defaultdict(set)
for incident in edge_faces.values():
for a in range(len(incident)):
for b in range(a + 1, len(incident)):
dual_adj[incident[a]].add(incident[b])
dual_adj[incident[b]].add(incident[a])
targets: list[frozenset[Any]] = []
seen = [False] * len(faces)
for start in range(len(faces)):
if seen[start]:
continue
depth = depths[start]
component = [start]
seen[start] = True
stack = [start]
while stack:
f = stack.pop()
for h in dual_adj[f]:
if not seen[h] and depths[h] == depth:
seen[h] = True
component.append(h)
stack.append(h)
inner: set[Any] = set()
for f in component:
inner.update(v for v in face_vertices[f] if distances[v] == depth + 1)
if len(inner) >= 4:
targets.append(frozenset(inner))
return targets
def first_inner_boundary_violation(
targets: Sequence[frozenset[Any]], coloring: Coloring
) -> tuple[frozenset[Any], set[int]] | None:
"""Return the first inner boundary using all four colours, if any."""
for inner in targets:
used = {coloring[v] for v in inner}
if len(used) > 3:
return inner, used
return None
def coloring_witness(
g: Graph,
source: Source,
max_colorings: int | None,
restriction: str,
) -> tuple[Coloring | None, int, bool]:
"""Find a proper 4-colouring satisfying the conjectured restriction.
Returns (witness, checked_count, exhausted). If witness is None and
exhausted is False, max_colorings was reached before a decision.
"""
distances = distances_from_source(g, source)
targets = (
inner_boundary_vertex_sets(g, source)
if restriction == "inner-boundary"
else None
)
checked = 0
for raw in all_graph_colorings(g, 4, vertex_color_dict=True):
coloring = cast(Coloring, raw)
checked += 1
if restriction == "inner-boundary":
violated = first_inner_boundary_violation(cast(Sequence, targets), coloring)
else:
violated = level_cycle_violation(g, distances, coloring)
if violated is None:
return coloring, checked, True
if max_colorings is not None and checked >= max_colorings:
return None, checked, False
return None, checked, True
def source_label(source: Source) -> str:
if len(source) == 1:
return f"vertex:{source[0]}"
return "cycle:{" + ",".join(str(v) for v in source) + "}"
def test_graph(
g: Graph,
sources: Iterable[Source],
max_colorings: int | None,
stop_first: bool,
quantifier: str,
restriction: str,
) -> tuple[bool, bool, int]:
"""Test a graph over selected sources.
Returns (passed, complete, sources_checked).
"""
checked_sources = 0
complete = True
found_any_source = False
for source in sources:
checked_sources += 1
witness, n_checked, exhausted = coloring_witness(
g, source, max_colorings, restriction
)
if witness is None:
if not exhausted:
complete = False
status = "FAIL" if exhausted else "UNKNOWN"
print(
f" {status}: source={source_label(source)}, "
f"colorings_checked={n_checked}"
)
if exhausted and quantifier == "all-sources":
if restriction == "level-cycle":
distances = distances_from_source(g, source)
first = next(
all_graph_colorings(g, 4, vertex_color_dict=True), None
)
if first is not None:
violation = level_cycle_violation(
g, distances, cast(Coloring, first)
)
print(f" first_coloring_violation={violation}")
return False, complete, checked_sources
if stop_first:
if quantifier == "all-sources":
return True, False, checked_sources
if not exhausted:
return True, False, checked_sources
else:
found_any_source = True
print(
f" pass: source={source_label(source)}, "
f"colorings_checked={n_checked}"
)
if quantifier == "exists-source":
return True, complete, checked_sources
if quantifier == "exists-source" and not found_any_source:
return False, complete, checked_sources
return True, complete, checked_sources
def parse_args() -> argparse.Namespace:
parser = argparse.ArgumentParser(description=__doc__)
parser.add_argument("n_min", type=int, nargs="?", default=4)
parser.add_argument("n_max", type=int, nargs="?", default=9)
parser.add_argument(
"--sources",
choices=("vertex", "cycle", "all"),
default="vertex",
help=(
"which candidate level sources to search; cycle means induced "
"cycle sources"
),
)
parser.add_argument(
"--quantifier",
choices=("exists-source", "all-sources"),
default="exists-source",
help=(
"exists-source tests the weakened conjecture; all-sources tests "
"the stronger earlier version"
),
)
parser.add_argument(
"--restriction",
choices=("level-cycle", "inner-boundary"),
default="level-cycle",
help=(
"level-cycle constrains every simple level cycle; inner-boundary "
"constrains only the tire inner boundaries of a vertex-rooted "
"tire-tree decomposition"
),
)
parser.add_argument(
"--max-cycle-source-size",
type=int,
default=None,
help="optional cap on induced cycle source size",
)
parser.add_argument(
"--min-connectivity",
type=int,
default=None,
help=(
"restrict to triangulations of at least this vertex connectivity "
"(e.g. 5 for the 5-connected slice); passed to plantri via Sage"
),
)
parser.add_argument(
"--max-colorings",
type=int,
default=None,
help="optional cap per graph/source; capped searches report UNKNOWN",
)
parser.add_argument(
"--full",
action="store_true",
help="continue after failures/unknowns instead of stopping at first",
)
return parser.parse_args()
def main() -> int:
args = parse_args()
stop_first = not args.full
if args.restriction == "inner-boundary" and args.sources != "vertex":
print(
"note: inner-boundary restriction is vertex-rooted; "
f"overriding --sources {args.sources} with vertex"
)
args.sources = "vertex"
total_graphs = 0
total_sources = 0
unknown = 0
triangulation_kwargs = {}
if args.min_connectivity is not None:
triangulation_kwargs["minimum_connectivity"] = args.min_connectivity
for n in range(args.n_min, args.n_max + 1):
print(f"=== n={n} ===")
for idx, g in enumerate(
graphs.triangulations(n, **triangulation_kwargs), start=1
):
total_graphs += 1
source_list = list(
level_sources(g, args.sources, args.max_cycle_source_size)
)
print(f" graph #{idx}: sources={len(source_list)}")
passed, complete, checked_sources = test_graph(
g,
source_list,
args.max_colorings,
stop_first,
args.quantifier,
args.restriction,
)
total_sources += checked_sources
if not complete:
unknown += 1
if not passed:
print(
f"COUNTEREXAMPLE candidate: n={n}, graph_index={idx}, "
f"source_mode={args.sources}, quantifier={args.quantifier}, "
f"restriction={args.restriction}"
)
print(f" edges={sorted(tuple(sorted(e)) for e in g.edges(labels=False))}")
return 1
if not complete and stop_first:
print(
f"UNKNOWN: n={n}, graph_index={idx}, "
f"source_mode={args.sources}, quantifier={args.quantifier}"
)
return 2
print(
f"PASS: checked {total_graphs} triangulations and {total_sources} "
f"sources; unknown_graphs={unknown}"
)
return 0 if unknown == 0 else 2
if __name__ == "__main__":
raise SystemExit(main())
@@ -0,0 +1,110 @@
"""Draw the 14-vertex counterexample to the tire inner-boundary
three-colour conjecture (Conjecture~\\ref{conj:tire-inner-boundary-three-colour}).
This is the graph at index 263993 in the n=14 plantri enumeration: a
3-connected (but not 5-connected) maximal planar graph with degree
sequence [7,7,7,7,7,7,6,6,3,3,3,3,3,3] and exactly 96 proper
4-colourings, none of which witness the inner-boundary restriction
from any vertex source.
"""
from __future__ import annotations
import os
import matplotlib.pyplot as plt
import networkx as nx
from matplotlib.lines import Line2D
OUT_DIR = os.path.dirname(os.path.dirname(os.path.abspath(__file__)))
EDGES = [
(1, 2), (1, 3), (1, 4), (1, 5), (1, 6), (1, 7), (1, 8),
(2, 3), (2, 4), (2, 6), (2, 8), (2, 9), (2, 10),
(3, 4), (4, 5), (4, 6), (4, 10),
(5, 6), (6, 7), (6, 9), (6, 10),
(7, 8), (7, 9), (7, 11), (7, 12), (7, 13),
(8, 9), (8, 12), (8, 13), (8, 14),
(9, 11), (9, 12), (9, 14),
(11, 12), (12, 13), (12, 14),
]
def build_graph() -> nx.Graph:
g = nx.Graph()
g.add_edges_from(EDGES)
return g
def main() -> int:
g = build_graph()
is_planar, _ = nx.check_planarity(g)
if not is_planar:
raise RuntimeError("graph should be planar")
pos = nx.planar_layout(g, scale=3.4)
fig, ax = plt.subplots(figsize=(8.2, 7.4))
nx.draw_networkx_edges(g, pos, ax=ax, edge_color="#cbd5e1", width=1.3)
deg3 = [v for v in g.nodes() if g.degree(v) == 3]
deg7 = [v for v in g.nodes() if g.degree(v) == 7]
other = [v for v in g.nodes() if v not in deg3 and v not in deg7]
def draw_nodes(nodes, color):
for v in nodes:
x, y = pos[v]
ax.scatter(
[x], [y],
s=520,
color=color,
edgecolors="black",
linewidths=1.1,
zorder=3,
)
ax.text(
x, y, f"{v}",
ha="center", va="center",
color="white", fontsize=11, fontweight="bold",
zorder=4,
)
draw_nodes(deg7, "#0f172a")
draw_nodes(other, "#475569")
draw_nodes(deg3, "#94a3b8")
legend = [
Line2D([0], [0], marker="o", color="w",
label=r"degree $7$",
markerfacecolor="#0f172a", markeredgecolor="black",
markersize=12),
Line2D([0], [0], marker="o", color="w",
label=r"degree $6$",
markerfacecolor="#475569", markeredgecolor="black",
markersize=12),
Line2D([0], [0], marker="o", color="w",
label=r"degree $3$",
markerfacecolor="#94a3b8", markeredgecolor="black",
markersize=12),
]
ax.legend(handles=legend, loc="lower center", ncol=3, framealpha=0.95)
ax.set_title(
"Counterexample to the inner-boundary three-colour conjecture "
"($n=14$)",
fontsize=13, pad=14,
)
ax.set_aspect("equal")
ax.axis("off")
fig.tight_layout(rect=[0, 0.05, 1, 1])
out = os.path.join(OUT_DIR, "fig_inner_boundary_counterexample.png")
fig.savefig(out, dpi=180, bbox_inches="tight")
plt.close(fig)
print(f"wrote {out}")
return 0
if __name__ == "__main__":
raise SystemExit(main())
@@ -0,0 +1,206 @@
"""Draw the medial tire graph for the tire example in Figure 2.
The example uses the same random tire parameters as fig_tire_example:
m=6, k=4, one chord of O, seed=3. The medial tire graph is built from
the plane graph obtained by omitting the chord edges of O, and then
deleting medial edges between two outer-boundary edges or two
inner-boundary edges. Its vertices are placed at the midpoints of the
retained tire edges.
"""
import os
import sys
HERE = os.path.dirname(os.path.abspath(__file__))
DUAL_EXP = os.path.abspath(
os.path.join(HERE, '..', '..', 'coloring_nested_tire_dual_graphs', 'experiments')
)
sys.path.insert(0, DUAL_EXP)
import matplotlib.pyplot as plt
import matplotlib.patches as patches
from tire_graph import random_tire, planar_positions
def edge_key(u, v):
return tuple(sorted((u, v)))
def is_inner_chord(edge, m, k):
u, v = edge
if not (m <= u < m + k and m <= v < m + k):
return False
a, b = u - m, v - m
d = abs(a - b)
return min(d, k - d) != 1
def is_outer_boundary_edge(edge, outer):
outer_set = set(outer)
if not set(edge) <= outer_set:
return False
m = len(outer)
idx = {v: i for i, v in enumerate(outer)}
a, b = idx[edge[0]], idx[edge[1]]
return (a - b) % m in (1, m - 1)
def is_inner_boundary_edge(edge, inner):
inner_set = set(inner)
if not set(edge) <= inner_set:
return False
k = len(inner)
idx = {v: i for i, v in enumerate(inner)}
a, b = idx[edge[0]], idx[edge[1]]
return (a - b) % k in (1, k - 1)
def suppress_boundary_medial_edge(e1, e2, outer, inner):
return (
is_outer_boundary_edge(e1, outer) and is_outer_boundary_edge(e2, outer)
) or (
is_inner_boundary_edge(e1, inner) and is_inner_boundary_edge(e2, inner)
)
def face_edges(face):
return [edge_key(face[i], face[(i + 1) % len(face)]) for i in range(len(face))]
def build_medial_tire(tire):
m, k = tire['m'], tire['k']
outer = tire['outer']
inner = tire['inner']
omitted = {edge_key(m + a, m + b) for a, b in tire['inner_chords']}
retained_edges = sorted(
edge_key(u, v)
for u, v in tire['edges']
if edge_key(u, v) not in omitted
)
retained = set(retained_edges)
faces = [tuple(tri) for tri in tire['triangles']]
faces.append(tuple(outer))
faces.append(tuple(reversed(inner)))
medial_edges = set()
for face in faces:
boundary = [e for e in face_edges(face) if e in retained]
for i, e in enumerate(boundary):
nxt = boundary[(i + 1) % len(boundary)]
if suppress_boundary_medial_edge(e, nxt, outer, inner):
continue
medial_edges.add(tuple(sorted((e, nxt))))
return retained_edges, sorted(medial_edges), omitted
def draw_medial_tire_graph(tire, filename):
m, k = tire['m'], tire['k']
outer_set = set(tire['outer'])
inner_set = set(tire['inner'])
pos = planar_positions(tire, R_out=1.0, R_in=0.45)
medial_vertices, medial_edges, omitted = build_medial_tire(tire)
medial_pos = {
e: ((pos[e[0]][0] + pos[e[1]][0]) / 2, (pos[e[0]][1] + pos[e[1]][1]) / 2)
for e in medial_vertices
}
C = {
'outer_cycle': '#1f77b4',
'inner_cycle': '#d62728',
'inner_chord': '#ff7f0e',
'annular': '#c7c7c7',
'medial_edge': '#0f766e',
'medial_vertex': '#134e4a',
}
fig, ax = plt.subplots(figsize=(7.2, 7.2))
for r in (1.04, 0.41):
ax.add_patch(patches.Circle((0, 0), r, fill=False,
edgecolor='lightgray',
linewidth=0.5, linestyle='--'))
for u, v in sorted(edge_key(u, v) for u, v in tire['edges']):
x1, y1 = pos[u]
x2, y2 = pos[v]
e = edge_key(u, v)
if e in omitted:
color, lw, ls, alpha = C['inner_chord'], 1.6, (0, (4, 3)), 0.45
elif u in outer_set and v in outer_set:
color, lw, ls, alpha = C['outer_cycle'], 2.0, '-', 0.35
elif u in inner_set and v in inner_set:
color, lw, ls, alpha = C['inner_cycle'], 2.0, '-', 0.35
else:
color, lw, ls, alpha = C['annular'], 1.0, '-', 0.55
ax.plot([x1, x2], [y1, y2], color=color, linewidth=lw,
linestyle=ls, alpha=alpha, zorder=1)
for e1, e2 in medial_edges:
x1, y1 = medial_pos[e1]
x2, y2 = medial_pos[e2]
ax.plot([x1, x2], [y1, y2], color=C['medial_edge'],
linewidth=1.8, alpha=0.92, zorder=3)
for idx, e in enumerate(medial_vertices):
x, y = medial_pos[e]
ax.scatter([x], [y], s=58, color=C['medial_vertex'],
edgecolors='white', linewidths=0.8, zorder=4)
ax.annotate(f"$m_{{{idx}}}$", (x, y), xytext=(3, 3),
textcoords='offset points', color=C['medial_vertex'],
fontsize=6.5, zorder=5)
for v in tire['outer']:
x, y = pos[v]
ax.scatter([x], [y], s=150, color=C['outer_cycle'],
edgecolors='white', linewidths=0.8, alpha=0.6, zorder=2)
for v in tire['inner']:
x, y = pos[v]
ax.scatter([x], [y], s=135, color=C['inner_cycle'],
edgecolors='white', linewidths=0.8, alpha=0.6, zorder=2)
legend_items = [
plt.Line2D([], [], color=C['medial_edge'], linewidth=1.8,
label=r'medial tire graph edge'),
plt.Line2D([], [], marker='o', color='w',
markerfacecolor=C['medial_vertex'], markeredgecolor='white',
markersize=7, label=r'medial vertex at an edge midpoint'),
plt.Line2D([], [], color=C['inner_chord'], linewidth=1.6,
linestyle=(0, (4, 3)), alpha=0.55,
label=r'chord of $O$ omitted from medial construction'),
plt.Line2D([], [], color=C['annular'], linewidth=1.0,
label=r'underlying tire graph, faint'),
]
ax.legend(handles=legend_items, loc='upper left',
bbox_to_anchor=(1.0, 1.0), fontsize=9, frameon=False)
ax.set_xlim(-1.24, 1.24)
ax.set_ylim(-1.24, 1.24)
ax.set_aspect('equal')
ax.axis('off')
ax.set_title(
r"Medial tire graph $M_{\mathrm{tire}}(T)$ for Figure 2's tire"
"\n"
r"midpoint vertices; no medial edges between consecutive boundary edges",
fontsize=11,
)
fig.savefig(filename, dpi=180, bbox_inches='tight')
plt.close(fig)
print(f"wrote {filename}")
print(f"retained tire edges: {len(medial_vertices)}")
print(f"medial edges: {len(medial_edges)}")
print(f"omitted O chords: {sorted(omitted)}")
def main():
paper_dir = os.path.abspath(os.path.join(HERE, '..'))
tire = random_tire(m=6, k=4, n_chords=1, seed=3)
out = os.path.join(paper_dir, 'fig_medial_tire_example.png')
draw_medial_tire_graph(tire, out)
if __name__ == '__main__':
main()
@@ -0,0 +1,195 @@
"""Draw the seam-realizability construction for Conjecture~\\ref{conj:seam-realizability}.
(a) Left: G_1, a stacked-ring triangulation with single-vertex level source
S_1 = {0}. Vertices coloured by BFS-from-S_1 level (0, 1, 2, 3).
The four colours visually correspond to the rooted tree of tire treads
of G_1 -- a chain T_0 -> T_1 -> T_2 with O^{(T_d)} = G_1[L_{d+1}] on
each tread.
(b) Right: H_5, the apex-removal seam construction. We take G_1 \\ {S_1}
(octahedron-like, 9 vertices) and re-embed so the former fan-face
around S_1 becomes the outer face, with L_1 as the new outer boundary
of that disk. We then attach a triangulated annulus A_5 from L_1 to a
fresh boundary 5-cycle, partial H_5. Vertices coloured by
BFS-from-(partial H_5) level.
Visual claim: the BFS level labels match between (a) and (b) on
V(G_1) \\ {S_1}; the new level-0 ring of (b) is the boundary cycle
partial H_5 of length k = 5, replacing the single-vertex source S_1 of (a).
Hence T(H_5, partial H_5) is iso (combinatorial, O-preserved) to T(G_1, S_1).
"""
import math
import os
import networkx as nx
import matplotlib.pyplot as plt
from matplotlib.lines import Line2D
OUT_DIR = os.path.dirname(os.path.dirname(os.path.abspath(__file__)))
# ---------------------------------------------------------------------------
# (a) Build G_1: source 0 + concentric triangular rings L_1, L_2, L_3.
# ---------------------------------------------------------------------------
RINGS = 3
pos_G = {0: (0.0, 0.0)}
ring_G = {0: [0]}
nxt = 1
for r in range(1, RINGS + 1):
ids = []
for j in range(3):
ang = math.radians(90 + 120 * j)
pos_G[nxt] = (r * math.cos(ang), r * math.sin(ang))
ids.append(nxt)
nxt += 1
ring_G[r] = ids
G1 = nx.Graph()
G1.add_nodes_from(pos_G)
for v in ring_G[1]:
G1.add_edge(0, v)
for r in range(1, RINGS + 1):
a, b, c = ring_G[r]
G1.add_edges_from([(a, b), (b, c), (c, a)])
for r in range(1, RINGS):
inner, outer = ring_G[r], ring_G[r + 1]
for j in range(3):
G1.add_edge(inner[j], outer[j]) # spoke
G1.add_edge(inner[j], outer[(j + 1) % 3]) # annulus diagonal
assert G1.number_of_edges() == 3 * G1.number_of_nodes() - 6, "G_1 not a triangulation"
level_G = nx.shortest_path_length(G1, source=0)
# ---------------------------------------------------------------------------
# (b) Build H_5: re-embed (G_1 \ {S_1}) so the former S_1 fan-face is the
# outer face (L_1 becomes the outer-most ring of that disk), then attach
# a triangulated annulus A_5 to a fresh 5-cycle partial H_5.
# ---------------------------------------------------------------------------
# Concentric placement: L_3 innermost (was G_1's outer face), L_1 outermost
# among G_1-derived vertices, partial H_5 outermost overall.
pos_H = {}
# Concentric placement with the SAME angles as panel (a): L_3 innermost,
# L_1 outermost among G_1-derived vertices. This is the topological flip
# (re-embedding) of (a); same vertex labels, same edges (minus S_1), but
# the ring with the smallest G_1-level is now at the largest radius.
RING_R = {1: 2.4, 2: 1.6, 3: 0.8}
for r in [1, 2, 3]:
for j, v in enumerate(ring_G[r]):
ang = math.radians(90 + 120 * j)
pos_H[v] = (RING_R[r] * math.cos(ang), RING_R[r] * math.sin(ang))
# partial H_5 vertices u0..u4 on a regular pentagon
BOUNDARY = [f'u{j}' for j in range(5)]
R_BDY = 3.6
for j, u in enumerate(BOUNDARY):
ang = math.radians(90 + 72 * j)
pos_H[u] = (R_BDY * math.cos(ang), R_BDY * math.sin(ang))
H = nx.Graph()
H.add_nodes_from(pos_H)
# inherit G_1 \ {S_1} edges, but recompute embedding rotations are positional
for u, v in G1.edges():
if 0 in (u, v):
continue
H.add_edge(u, v)
# partial H_5 cycle (the new outer boundary)
boundary_edges = [(BOUNDARY[j], BOUNDARY[(j + 1) % 5]) for j in range(5)]
H.add_edges_from(boundary_edges)
# annular edges A_5: a, b, c (= ring_G[1]) match to consecutive u_i ranges
a, b, c = ring_G[1]
annular_pairs = [
(a, 'u0'), (a, 'u1'), (a, 'u2'),
(b, 'u2'), (b, 'u3'), (b, 'u4'),
(c, 'u4'), (c, 'u0'),
]
H.add_edges_from(annular_pairs)
# H is a triangulated planar disk: all bounded faces triangles, outer face
# the 5-cycle partial H_5. Verify edge count by Euler with f outer = 5-gon:
# t bounded triangles, F = t + 1, V - E + F = 2 => E = V + t - 1;
# 3t + 5 = 2E => t = 2V - 7. Here V = 14, so t = 21, E = 34.
assert H.number_of_edges() == 34, f"unexpected edge count {H.number_of_edges()}"
level_H = nx.multi_source_dijkstra_path_length(H, set(BOUNDARY))
# Verify the seam claim: BFS levels on V(G_1) \ {S_1} match between G_1 and H.
for v in G1.nodes():
if v == 0:
continue
assert level_H[v] == level_G[v], (
f"level mismatch at v={v}: G_1 level {level_G[v]}, H level {level_H[v]}"
)
# ---------------------------------------------------------------------------
# Draw.
# ---------------------------------------------------------------------------
LEVEL_COLOR = {0: '#1e293b', 1: '#475569', 2: '#94a3b8', 3: '#cbd5e1'}
fig, axes = plt.subplots(1, 2, figsize=(16, 8.5))
def draw_panel(ax, graph, pos, levels, title, *, boundary=None, annular=None):
nx.draw_networkx_edges(graph, pos, ax=ax, edge_color='#d1d5db', width=1.2)
if annular:
nx.draw_networkx_edges(graph, pos, edgelist=annular, ax=ax,
edge_color='#f59e0b', width=1.8)
if boundary:
nx.draw_networkx_edges(graph, pos, edgelist=boundary, ax=ax,
edge_color='#dc2626', width=2.4)
for v, (x, y) in pos.items():
lev = levels[v]
ax.scatter([x], [y], s=560, color=LEVEL_COLOR[lev],
edgecolors='black', linewidths=1.0, zorder=3)
ax.text(x, y, f'{v}\n$\\ell{{=}}{lev}$', ha='center', va='center',
color='white', fontsize=8.5, fontweight='bold', zorder=4)
ax.set_aspect('equal')
ax.axis('off')
ax.set_title(title, fontsize=11)
draw_panel(
axes[0], G1, pos_G, level_G,
r"$(a)$ $G_1$ with single-vertex source $S_1 = \{0\}$." "\n"
r"BFS from $S_1$ gives levels $\ell = 0, 1, 2, 3$ "
r"(rings $\{0\}, L_1, L_2, L_3$).",
)
draw_panel(
axes[1], H, pos_H, level_H,
r"$(b)$ $H_5$: apex-removal seam." "\n"
r"Outer 5-cycle $\partial H_5$ (red) replaces $S_1$; "
r"annulus $A_5$ (orange) glues $\partial H_5$ to $L_1$.",
boundary=boundary_edges, annular=annular_pairs,
)
legend = [
Line2D([0], [0], marker='o', color='w', label=r'level $\ell = 0$',
markerfacecolor=LEVEL_COLOR[0], markeredgecolor='black', markersize=12),
Line2D([0], [0], marker='o', color='w', label=r'level $\ell = 1$ ($L_1$)',
markerfacecolor=LEVEL_COLOR[1], markeredgecolor='black', markersize=12),
Line2D([0], [0], marker='o', color='w', label=r'level $\ell = 2$ ($L_2$)',
markerfacecolor=LEVEL_COLOR[2], markeredgecolor='black', markersize=12),
Line2D([0], [0], marker='o', color='w', label=r'level $\ell = 3$ ($L_3$)',
markerfacecolor=LEVEL_COLOR[3], markeredgecolor='black', markersize=12),
Line2D([0], [0], color='#dc2626', lw=2.4, label=r'$\partial H_5$ (boundary $k$-cycle, $k=5$)'),
Line2D([0], [0], color='#f59e0b', lw=1.8, label=r'annulus $A_5$ edges'),
]
fig.legend(handles=legend, loc='lower center', ncol=3, fontsize=10, framealpha=0.95)
fig.suptitle(
r"Seam realizability (Conjecture 1.22): "
r"$\mathcal{T}(H_5, \partial H_5) \cong \mathcal{T}(G_1, S_1)$ "
r"as rooted trees of tire treads (combinatorial, $O$-preserved). "
r"BFS distances from $\partial H_5$ in $H_5$ reproduce $\ell_{G_1}$ "
r"on $V(G_1) \setminus \{S_1\}$.", fontsize=12,
)
fig.tight_layout(rect=[0, 0.08, 1, 0.95])
out = os.path.join(OUT_DIR, 'fig_seam_construction.png')
fig.savefig(out, dpi=180, bbox_inches='tight')
plt.close(fig)
print(f'G_1: |V|={G1.number_of_nodes()}, |E|={G1.number_of_edges()}, '
f'levels: {sorted(set(level_G.values()))}')
print(f'H_5: |V|={H.number_of_nodes()}, |E|={H.number_of_edges()}, '
f'levels: {sorted(set(level_H.values()))}')
print(f'wrote {out}')
@@ -0,0 +1,480 @@
"""Draw the tire-tree decomposition for Theorem~\\ref{thm:tire-tree-decomposition}.
Uses a Tutte embedding (barycentric solve with the outer face fixed on a
convex polygon) to give a planar straight-line layout.
Panel (a): G with 13 vertices, 5 levels (v_0 at level 0; L_1, L_2, L_3, L_4
on subsequent levels). Tutte outer face = h-g_1-g_2 (the deepest face from
v_0), so v_0 ends up roughly central and the outer triangle is "outermost"
in BFS-from-v_0 distance. Tree-of-treads has 5 nodes:
T_0
/ \\
T_R T_L
|
T_LL
|
T_LLL
Panel (b): G_{T_L} on 10 vertices, with Tutte outer face = C_{T_L} = {a,c,d}.
Levels in G_{T_L} satisfy ell_{G_{T_L}}(.) = ell_G(.) - 1 on V(G_{T_L});
T(G_{T_L}, C_{T_L}) is the chain T_L -> T_LL -> T_LLL.
"""
import math
import os
import networkx as nx
import numpy as np
import matplotlib.pyplot as plt
from matplotlib.lines import Line2D
OUT_DIR = os.path.dirname(os.path.dirname(os.path.abspath(__file__)))
# ---------------------------------------------------------------------------
# Build G.
# ---------------------------------------------------------------------------
G = nx.Graph()
G.add_nodes_from(['v0', 'a', 'b', 'c', 'd', 'e',
'f1', 'f2', 'f3', 'g1', 'g2', 'g3', 'h'])
# v_0 fan
for v in ['a', 'b', 'c', 'd']:
G.add_edge('v0', v)
# L_1 4-cycle
G.add_edges_from([('a', 'b'), ('b', 'c'), ('c', 'd'), ('d', 'a')])
# Chord a-c (outside L_1 in the planar embedding)
G.add_edge('a', 'c')
# e-fan (Region R)
for v in ['a', 'b', 'c']:
G.add_edge('e', v)
# f-triangle (Region L)
G.add_edges_from([('f1', 'f2'), ('f2', 'f3'), ('f3', 'f1')])
# Annular L_1 -> f-triangle: f_1~{a,d}, f_2~{d,c}, f_3~{a,c}
G.add_edges_from([
('f1', 'a'), ('f1', 'd'),
('f2', 'd'), ('f2', 'c'),
('f3', 'a'), ('f3', 'c'),
])
# g-triangle (inside f-triangle)
G.add_edges_from([('g1', 'g2'), ('g2', 'g3'), ('g3', 'g1')])
# Annular f-triangle -> g-triangle: f_1~{g_1, g_3}, f_2~{g_2, g_3}, f_3~{g_1, g_2}
G.add_edges_from([
('f1', 'g1'), ('f1', 'g3'),
('f2', 'g2'), ('f2', 'g3'),
('f3', 'g1'), ('f3', 'g2'),
])
# h-fan (inside g-triangle)
for v in ['g1', 'g2', 'g3']:
G.add_edge('h', v)
assert G.number_of_edges() == 3 * G.number_of_nodes() - 6, (
f"G not a triangulation: |E|={G.number_of_edges()}, "
f"expected {3 * G.number_of_nodes() - 6}"
)
level_G = nx.shortest_path_length(G, source='v0')
# ---------------------------------------------------------------------------
# Tutte embedding.
# ---------------------------------------------------------------------------
def tutte_embedding(graph, outer_face_cyclic, outer_radius=3.0,
angle_offset_deg=90.0, outer_weight=1.0):
"""Compute (weighted) Tutte embedding.
outer_face_cyclic: list of vertices on the outer face, in cyclic order.
Outer vertices are fixed on a regular polygon of given radius; every
interior vertex is placed at a convex combination of its neighbours'
positions (solved as a linear system). Edges incident to an outer
vertex carry weight `outer_weight`; interior-interior edges carry
weight 1. All weights positive, so Tutte's theorem still gives a
planar straight-line embedding. Larger `outer_weight` pulls interior
vertices more strongly toward the outer triangle, spreading them out.
"""
n_outer = len(outer_face_cyclic)
outer_positions = {}
for i, v in enumerate(outer_face_cyclic):
angle = math.radians(angle_offset_deg + i * 360 / n_outer)
outer_positions[v] = (outer_radius * math.cos(angle),
outer_radius * math.sin(angle))
outer_set = set(outer_face_cyclic)
interior = [v for v in graph.nodes() if v not in outer_set]
interior_idx = {v: i for i, v in enumerate(interior)}
m = len(interior)
if m == 0:
return outer_positions
A = np.zeros((m, m))
bx = np.zeros(m)
by = np.zeros(m)
for v in interior:
i = interior_idx[v]
for u in graph.neighbors(v):
w = outer_weight if u in outer_set else 1.0
A[i, i] += w
if u in outer_set:
bx[i] += w * outer_positions[u][0]
by[i] += w * outer_positions[u][1]
else:
j = interior_idx[u]
A[i, j] -= w
x = np.linalg.solve(A, bx)
y = np.linalg.solve(A, by)
pos = dict(outer_positions)
for v in interior:
i = interior_idx[v]
pos[v] = (float(x[i]), float(y[i]))
return pos
def stretch_radially(pos, outer_face_cyclic, alpha=0.6):
"""Stretch interior positions radially outward from the outer-face centroid.
Outer vertices are unchanged; for each interior vertex at radius r from
the outer-face centroid, replace r by r' = R^(1-alpha) * r^alpha, where
R is the radius of the outer vertices. With alpha < 1 this is a concave
stretch that pushes small radii outward. Angles are preserved, so
planarity of the underlying Tutte embedding is preserved.
"""
outer_set = set(outer_face_cyclic)
outer_positions = [pos[v] for v in outer_face_cyclic]
Cx = sum(p[0] for p in outer_positions) / len(outer_positions)
Cy = sum(p[1] for p in outer_positions) / len(outer_positions)
R = max(math.sqrt((p[0] - Cx)**2 + (p[1] - Cy)**2)
for p in outer_positions)
new_pos = {}
for v, p in pos.items():
if v in outer_set:
new_pos[v] = p
continue
dx, dy = p[0] - Cx, p[1] - Cy
r = math.sqrt(dx * dx + dy * dy)
if r < 1e-10:
new_pos[v] = (Cx, Cy)
continue
r_new = (R ** (1 - alpha)) * (r ** alpha)
scale = r_new / r
new_pos[v] = (Cx + dx * scale, Cy + dy * scale)
return new_pos
# Panel (a) positions: hand-tuned in TikZiT and copied back here so the
# matplotlib panel matches the .tikz layout the user is editing on Desktop.
# The chord a-c is drawable as a straight line at these positions; the
# d-a edge passes through f_1, so it's drawn as a slight Bezier curve.
pos_G = {
'v0': ( 0.00, 6.0),
'a': (-5.50, -5.0),
'b': (-2.75, 3.0),
'c': ( 1.75, 3.0),
'd': ( 8.00, -5.0),
'e': (-1.50, 1.5),
'f1': ( 1.50, -5.0),
'f2': ( 4.00, -1.0),
'f3': (-0.75, -1.0),
'g1': ( 0.70, -3.0),
'g2': ( 1.45, -1.5),
'g3': ( 2.30, -3.0),
'h': ( 1.55, -2.5),
}
# ---------------------------------------------------------------------------
# G_{T_L}: subgraph inside C_{T_L} = {a, c, d}.
# ---------------------------------------------------------------------------
C_TL = {'a', 'c', 'd'}
V_GTL = C_TL | {'f1', 'f2', 'f3', 'g1', 'g2', 'g3', 'h'}
G_TL = G.subgraph(V_GTL).copy()
level_GTL = nx.multi_source_dijkstra_path_length(G_TL, C_TL)
for v in V_GTL:
assert level_GTL[v] == level_G[v] - 1
# Tutte for G_{T_L}: outer face = a-d-c (= C_{T_L}, the seam itself).
# Cyclic order matches the planar boundary: a -> d -> c.
outer_face_GTL = ['a', 'd', 'c']
pos_GTL = tutte_embedding(G_TL, outer_face_GTL, outer_radius=2.8,
angle_offset_deg=90, outer_weight=3.0)
pos_GTL = stretch_radially(pos_GTL, outer_face_GTL, alpha=0.6)
# ---------------------------------------------------------------------------
# Edge sets.
# ---------------------------------------------------------------------------
C_TR_edges = [('a', 'b'), ('b', 'c'), ('a', 'c')]
C_TL_edges = [('a', 'd'), ('d', 'c'), ('a', 'c')]
C_TLL_edges = [('f1', 'f2'), ('f2', 'f3'), ('f3', 'f1')]
C_TLLL_edges = [('g1', 'g2'), ('g2', 'g3'), ('g3', 'g1')]
fan_edges = [('v0', v) for v in ['a', 'b', 'c', 'd']]
# ---------------------------------------------------------------------------
# Tree inset helper.
# ---------------------------------------------------------------------------
def draw_tree_inset(parent_ax, position, tree_nodes, tree_edges, node_pos,
label_text, highlight=None, title=None,
xlim=(-1.4, 1.4), ylim=(-3.6, 0.6)):
ax = parent_ax.inset_axes(position)
for u, v in tree_edges:
x0, y0 = node_pos[u]
x1, y1 = node_pos[v]
ax.plot([x0, x1], [y0, y1], color='black', lw=1.4, zorder=1)
for n in tree_nodes:
x, y = node_pos[n]
is_hi = highlight and n in highlight
ax.scatter([x], [y], s=380, color='#fde68a' if is_hi else '#e5e7eb',
edgecolors='black', linewidths=1.8 if is_hi else 1.0, zorder=3)
ax.text(x, y, label_text[n], ha='center', va='center',
fontsize=7.5, fontweight='bold', zorder=4)
ax.set_xlim(*xlim); ax.set_ylim(*ylim)
ax.set_aspect('equal')
ax.set_xticks([]); ax.set_yticks([])
if title:
ax.set_title(title, fontsize=8.5, pad=2)
for spine in ax.spines.values():
spine.set_edgecolor('#9ca3af')
spine.set_linewidth(0.8)
ax.patch.set_facecolor('#f9fafb')
# ---------------------------------------------------------------------------
# Draw.
# ---------------------------------------------------------------------------
LEVEL_COLOR = {
0: '#1e293b',
1: '#475569',
2: '#94a3b8',
3: '#cbd5e1',
4: '#f1f5f9',
}
fig, axes = plt.subplots(1, 2, figsize=(16, 9))
def _vertex_label(name):
"""Render 'f1' as 'f_1' (subscript) and 'v0' as 'v_0' for display."""
if len(name) >= 2 and name[0].isalpha() and name[1:].isdigit():
return f'{name[0]}_{{{name[1:]}}}'
return name
def draw_panel(ax, graph, pos, levels, seams, fan, title, xlim, ylim,
text_color_threshold=4, label_map=None):
"""seams: list of (edges, color, width) tuples; fan: edges list or None.
label_map: optional dict mapping vertex names to displayed names (so the
panel can show a relabelled version of the graph)."""
nx.draw_networkx_edges(graph, pos, ax=ax, edge_color='#d1d5db', width=1.1)
if fan is not None:
nx.draw_networkx_edges(graph, pos, edgelist=fan, ax=ax,
edge_color='#3b82f6', width=1.5, style='dashed')
for edges, color, width in seams:
nx.draw_networkx_edges(graph, pos, edgelist=edges, ax=ax,
edge_color=color, width=width)
for v, (x, y) in pos.items():
lev = levels[v]
text_color = 'white' if lev < text_color_threshold else 'black'
display_name = (label_map or {}).get(v, v)
ax.scatter([x], [y], s=520, color=LEVEL_COLOR[lev],
edgecolors='black', linewidths=1.0, zorder=3)
ax.text(x, y, f'${_vertex_label(display_name)}$\n$\\ell{{=}}{lev}$',
ha='center', va='center',
color=text_color, fontsize=7, fontweight='bold', zorder=4)
ax.set_aspect('equal')
ax.axis('off')
ax.set_xlim(*xlim); ax.set_ylim(*ylim)
ax.set_title(title, fontsize=10.5, pad=5)
# Compute panel limits from the Tutte positions, with padding.
def compute_limits(pos, pad=0.5):
xs = [p[0] for p in pos.values()]
ys = [p[1] for p in pos.values()]
return (min(xs) - pad, max(xs) + pad), (min(ys) - pad, max(ys) + pad)
xlim_a, ylim_a = compute_limits(pos_G, pad=0.6)
xlim_b, ylim_b = compute_limits(pos_GTL, pad=0.6)
# ============================================================================
# Panel (a): G -- positions match Desktop/tire_tree_decomposition.tikz.
# Draw all non-seam edges as plain gray (no separate dashed fan style here,
# to match the TikZiT version). Edge a-d at y = -5 would pass through f_1
# if drawn straight, so we render it (and seam C_{T_L}'s a-d component) as
# a slight Bezier curve via FancyArrowPatch.
# ============================================================================
ax = axes[0]
# Non-seam edges as straight gray lines; a-d and v_0-a are drawn curved
# below.
_curved_pairs = [{'a', 'd'}, {'v0', 'a'}]
non_seam_edges = [e for e in G.edges
if set(e) not in _curved_pairs
and set(e) not in (set(s) for s in C_TR_edges + C_TL_edges
+ C_TLL_edges + C_TLLL_edges)]
nx.draw_networkx_edges(G, pos_G, edgelist=non_seam_edges, ax=ax,
edge_color='#d1d5db', width=1.1)
# Curved edges (FancyArrowPatch). a-d dodges f_1; v_0-a is bent for
# visual balance (mirrors the TikZiT `bend right`).
from matplotlib.patches import FancyArrowPatch
def add_curved(ax, p_from, p_to, *, color, lw, rad, ls='-', zorder=2):
ax.add_patch(FancyArrowPatch(
posA=p_from, posB=p_to,
arrowstyle='-', connectionstyle=f'arc3,rad={rad}',
color=color, linewidth=lw, linestyle=ls, zorder=zorder,
))
add_curved(ax, pos_G['a'], pos_G['d'], color='#d1d5db', lw=1.1, rad=0.15)
add_curved(ax, pos_G['v0'], pos_G['a'], color='#d1d5db', lw=1.1, rad=0.25)
# Seams (straight, since the layout is now planar with straight chord).
# Order: bottom first (C_{T_LL}, C_{T_LLL}), then chord/L_1 seams on top.
nx.draw_networkx_edges(G, pos_G,
edgelist=[('f1', 'f2'), ('f2', 'f3'), ('f3', 'f1')],
ax=ax, edge_color='#9333ea', width=2.2)
nx.draw_networkx_edges(G, pos_G,
edgelist=[('g1', 'g2'), ('g2', 'g3'), ('g3', 'g1')],
ax=ax, edge_color='#0d9488', width=2.0)
nx.draw_networkx_edges(G, pos_G,
edgelist=[('a', 'b'), ('b', 'c')],
ax=ax, edge_color='#ea580c', width=2.4)
nx.draw_networkx_edges(G, pos_G,
edgelist=[('a', 'c'), ('d', 'c')],
ax=ax, edge_color='#dc2626', width=2.8)
add_curved(ax, pos_G['a'], pos_G['d'], color='#dc2626', lw=2.8, rad=0.15, zorder=4)
# Vertices.
for v, (x, y) in pos_G.items():
lev = level_G[v]
text_color = 'white' if lev < 4 else 'black'
ax.scatter([x], [y], s=520, color=LEVEL_COLOR[lev],
edgecolors='black', linewidths=1.0, zorder=5)
ax.text(x, y, f'${_vertex_label(v)}$\n$\\ell{{=}}{lev}$',
ha='center', va='center',
color=text_color, fontsize=7, fontweight='bold', zorder=6)
ax.set_aspect('equal')
ax.axis('off')
# The a-d arc bulges below y=-5 by ~ rad * |a - d| / 2 ≈ 1.0 with rad=0.15;
# pad the y range so it isn't clipped.
xlim_a, ylim_a = compute_limits(pos_G, pad=0.8)
ylim_a = (ylim_a[0] - 1.2, ylim_a[1])
ax.set_xlim(*xlim_a); ax.set_ylim(*ylim_a)
ax.set_title(
r"$(a)$ $G$: 13 vertices, BFS levels $\ell_G \in \{0,1,2,3,4\}$,"
"\n"
r"four nested seams $C_{T_R}, C_{T_L}, C_{T_{LL}}, C_{T_{LLL}}$ "
r"(chord $a$-$c$ drawn straight in this layout).",
fontsize=10.5, pad=5,
)
tree_pos_a = {
'T_0': (0.0, 0.0),
'T_R': (-0.7, -1.0),
'T_L': (0.7, -1.0),
'T_LL': (0.7, -2.0),
'T_LLL': (0.7, -3.0),
}
tree_labels = {
'T_0': r'$T_0$', 'T_R': r'$T_R$', 'T_L': r'$T_L$',
'T_LL': r'$T_{LL}$', 'T_LLL': r'$T_{LLL}$',
}
draw_tree_inset(
axes[0], [0.70, 0.42, 0.28, 0.55],
tree_nodes=['T_0', 'T_R', 'T_L', 'T_LL', 'T_LLL'],
tree_edges=[('T_0', 'T_R'), ('T_0', 'T_L'),
('T_L', 'T_LL'), ('T_LL', 'T_LLL')],
node_pos=tree_pos_a, label_text=tree_labels,
highlight={'T_L', 'T_LL', 'T_LLL'},
title=r'$\mathcal{T}(G, \{v_0\})$',
xlim=(-1.4, 1.4), ylim=(-3.6, 0.6),
)
# ============================================================================
# Panel (b): G_{T_L}. Vertex names are rotated relative to the parent G
# (a->c, c->d, d->a; f_1->f_3, f_2->f_1, f_3->f_2; g_1->g_2, g_2->g_3,
# g_3->g_1; h stays h) -- the relabelling emphasises the new role of
# C_{T_L} as cycle source, with the boundary now naturally read as
# {a, c, d} in cyclic order from a position the user picked.
# ============================================================================
GTL_LABEL_MAP = {
'a': 'c', 'c': 'd', 'd': 'a',
'f1': 'f3', 'f2': 'f1', 'f3': 'f2',
'g1': 'g2', 'g2': 'g3', 'g3': 'g1',
'h': 'h',
}
draw_panel(
axes[1], G_TL, pos_GTL, level_GTL,
seams=[
(C_TL_edges, '#dc2626', 2.8),
(C_TLL_edges, '#9333ea', 2.2),
(C_TLLL_edges, '#0d9488', 2.0),
],
fan=None,
title=(
r"$(b)$ $G_{T_L}$ (Tutte embedding, outer face $C_{T_L} = \{a,c,d\}$):"
" 10 vertices, cycle source $C_{T_L}$,\n"
r"$\ell_{G_{T_L}}(\cdot) = \ell_G(\cdot) - 1$; "
r"$\mathcal{T}(G_{T_L}, C_{T_L})$ is the chain $T_L \to T_{LL} \to T_{LLL}$."
),
xlim=xlim_b, ylim=ylim_b,
text_color_threshold=3,
label_map=GTL_LABEL_MAP,
)
sub_tree_pos = {
'T_L': (0.0, 0.0),
'T_LL': (0.0, -1.0),
'T_LLL': (0.0, -2.0),
}
draw_tree_inset(
axes[1], [0.70, 0.42, 0.28, 0.55],
tree_nodes=['T_L', 'T_LL', 'T_LLL'],
tree_edges=[('T_L', 'T_LL'), ('T_LL', 'T_LLL')],
node_pos=sub_tree_pos, label_text=tree_labels,
highlight={'T_L', 'T_LL', 'T_LLL'},
title=r'$\mathcal{T}(G_{T_L}, C_{T_L})$',
xlim=(-1.0, 1.0), ylim=(-2.6, 0.4),
)
# ============================================================================
# Legend + suptitle
# ============================================================================
legend = [
Line2D([0], [0], marker='o', color='w', label=r'$\ell = 0$',
markerfacecolor=LEVEL_COLOR[0], markeredgecolor='black', markersize=10),
Line2D([0], [0], marker='o', color='w', label=r'$\ell = 1$',
markerfacecolor=LEVEL_COLOR[1], markeredgecolor='black', markersize=10),
Line2D([0], [0], marker='o', color='w', label=r'$\ell = 2$',
markerfacecolor=LEVEL_COLOR[2], markeredgecolor='black', markersize=10),
Line2D([0], [0], marker='o', color='w', label=r'$\ell = 3$',
markerfacecolor=LEVEL_COLOR[3], markeredgecolor='black', markersize=10),
Line2D([0], [0], marker='o', color='w', label=r'$\ell = 4$',
markerfacecolor=LEVEL_COLOR[4], markeredgecolor='black', markersize=10),
Line2D([0], [0], color='#ea580c', lw=2.4, label=r'seam $C_{T_R}$'),
Line2D([0], [0], color='#dc2626', lw=2.8, label=r'seam $C_{T_L}$'),
Line2D([0], [0], color='#9333ea', lw=2.2, label=r'seam $C_{T_{LL}}$'),
Line2D([0], [0], color='#0d9488', lw=2.0, label=r'seam $C_{T_{LLL}}$'),
]
fig.legend(handles=legend, loc='lower center', ncol=5, fontsize=9.5,
framealpha=0.95, columnspacing=1.8)
fig.suptitle(
r"Tire-tree decomposition (Theorem 1.19): every tread $T$ is the root "
r"of its own tree of tire treads $\mathcal{T}(G_T, C_T)$.",
fontsize=12, y=0.96,
)
fig.subplots_adjust(top=0.88, bottom=0.16, left=0.02, right=0.98, wspace=0.05)
out = os.path.join(OUT_DIR, 'fig_tire_tree_decomposition.png')
fig.savefig(out, dpi=180, bbox_inches='tight')
plt.close(fig)
print(f'G: |V|={G.number_of_nodes()}, |E|={G.number_of_edges()}, '
f'levels {sorted(set(level_G.values()))}')
print(f'G_TL: |V|={G_TL.number_of_nodes()}, |E|={G_TL.number_of_edges()}, '
f'levels {sorted(set(level_GTL.values()))}')
print(f'verified level shift (D2): ell_GTL(v) = ell_G(v) - 1 for all '
f'{len(V_GTL)} v in V(G_TL)')
print(f'panel (a): hand-tuned positions (see Desktop/tire_tree_decomposition.tikz)')
print(f'Tutte (G_TL): outer face = {outer_face_GTL}')
print(f'wrote {out}')
@@ -0,0 +1,132 @@
"""Draw the 8-vertex counterexample to the universal-source form.
The figure highlights the source vertex 7, the two BFS levels, and the
level cycle (3,4,5,8) that forces all four colours for that source.
"""
from __future__ import annotations
import os
import matplotlib.pyplot as plt
import networkx as nx
from matplotlib.lines import Line2D
OUT_DIR = os.path.dirname(os.path.dirname(os.path.abspath(__file__)))
def build_graph() -> nx.Graph:
g = nx.Graph()
g.add_edges_from(
[
(1, 2), (1, 3), (1, 4), (1, 5), (1, 6), (1, 7),
(2, 3), (2, 6), (2, 7),
(3, 4), (3, 5), (3, 6), (3, 8),
(4, 5),
(5, 6), (5, 8),
(6, 7), (6, 8),
]
)
return g
def main() -> int:
g = build_graph()
levels = nx.single_source_shortest_path_length(g, 7)
is_planar, embedding = nx.check_planarity(g)
if not is_planar:
raise RuntimeError("counterexample graph should be planar")
pos = nx.planar_layout(g, scale=3.4)
fig, ax = plt.subplots(figsize=(8.6, 7.2))
nx.draw_networkx_edges(g, pos, ax=ax, edge_color="#cbd5e1", width=1.4)
cycle_edges = [(3, 4), (4, 5), (5, 8), (8, 3)]
nx.draw_networkx_edges(
g,
pos,
ax=ax,
edgelist=cycle_edges,
edge_color="#dc2626",
width=2.8,
)
level_colors = {0: "#0f172a", 1: "#475569", 2: "#94a3b8"}
for v, (x, y) in pos.items():
lev = levels[v]
ax.scatter(
[x],
[y],
s=600 if v == 7 else 500,
color=level_colors[lev],
edgecolors="black",
linewidths=1.1,
zorder=3,
)
ax.text(
x,
y,
f"{v}\n$\\ell={lev}$",
ha="center",
va="center",
color="white",
fontsize=10,
fontweight="bold",
zorder=4,
)
legend = [
Line2D(
[0],
[0],
marker="o",
color="w",
label=r"source $S=\{7\}$",
markerfacecolor=level_colors[0],
markeredgecolor="black",
markersize=12,
),
Line2D(
[0],
[0],
marker="o",
color="w",
label=r"level $L_1$",
markerfacecolor=level_colors[1],
markeredgecolor="black",
markersize=12,
),
Line2D(
[0],
[0],
marker="o",
color="w",
label=r"level $L_2$",
markerfacecolor=level_colors[2],
markeredgecolor="black",
markersize=12,
),
Line2D([0], [0], color="#dc2626", lw=2.8, label=r"problem cycle $(3,4,5,8)$"),
]
ax.legend(handles=legend, loc="lower center", ncol=2, framealpha=0.95)
ax.set_title(
"Counterexample to the universal-source form",
fontsize=14,
pad=18,
)
ax.set_aspect("equal")
ax.axis("off")
fig.tight_layout(rect=[0, 0.05, 1, 1])
out = os.path.join(OUT_DIR, "fig_universal_level_cycle_counterexample.png")
fig.savefig(out, dpi=180, bbox_inches="tight")
plt.close(fig)
print(f"wrote {out}")
return 0
if __name__ == "__main__":
raise SystemExit(main())
@@ -0,0 +1,189 @@
"""Generate and test candidate graph families for the level-cycle conjecture.
This script builds a few rigid maximal planar families and then runs the
existing level-cycle checker on them. It is meant as a small Sage-side
driver for probing likely counterexample sources before moving on to larger
families.
Available families:
stacked-ring concentric triangular rings like the paper's G_1
face-stack a chain of stacked triangulations built by repeatedly
stacking a vertex into a triangular face
Examples:
sage -python experiments/generate_candidate_families.py stacked-ring 1 6
sage -python experiments/generate_candidate_families.py face-stack 4 12 --full
"""
from __future__ import annotations
import argparse
import logging
from typing import Callable
from sage.all import Graph # type: ignore[attr-defined] # pylint: disable=no-name-in-module
from check_level_cycle_three_color import level_sources, test_graph
LOGGER = logging.getLogger(__name__)
def build_stacked_ring(levels: int) -> Graph:
"""Return the concentric triangular-ring family used in the paper figure."""
if levels < 1:
raise ValueError("stacked-ring requires at least one ring")
g = Graph()
g.add_vertex(0)
next_vertex = 1
ring1 = [next_vertex + i for i in range(3)]
next_vertex += 3
g.add_vertices(ring1)
g.add_edges([(0, v) for v in ring1])
g.add_edges([(ring1[i], ring1[(i + 1) % 3]) for i in range(3)])
inner = ring1
for _ in range(1, levels):
outer = [next_vertex + i for i in range(3)]
next_vertex += 3
g.add_vertices(outer)
g.add_edges([(outer[i], outer[(i + 1) % 3]) for i in range(3)])
g.add_edges([(inner[i], outer[i]) for i in range(3)])
g.add_edges([(inner[i], outer[(i + 1) % 3]) for i in range(3)])
inner = outer
expected_edges = 3 * g.n_vertices() - 6
if g.num_edges() != expected_edges:
raise AssertionError(
f"stacked-ring is not maximal planar: |V|={g.n_vertices()}, "
f"|E|={g.num_edges()}, expected {expected_edges}"
)
return g
def build_face_stack(steps: int) -> Graph:
"""Return a stacked triangulation built by repeatedly subdividing one face."""
if steps < 1:
raise ValueError("face-stack requires at least one step")
g = Graph()
g.add_vertices([0, 1, 2, 3])
g.add_edges([(0, 1), (1, 2), (2, 0)])
g.add_edges([(3, 0), (3, 1), (3, 2)])
active_face = (0, 1, 3)
next_vertex = 4
for _ in range(steps - 1):
v = next_vertex
next_vertex += 1
a, b, c = active_face
g.add_vertex(v)
g.add_edges([(v, a), (v, b), (v, c)])
active_face = (a, c, v)
expected_edges = 3 * g.n_vertices() - 6
if g.num_edges() != expected_edges:
raise AssertionError(
f"face-stack is not maximal planar: |V|={g.n_vertices()}, "
f"|E|={g.num_edges()}, expected {expected_edges}"
)
return g
FAMILY_BUILDERS: dict[str, Callable[[int], Graph]] = {
"stacked-ring": build_stacked_ring,
"face-stack": build_face_stack,
}
def parse_args() -> argparse.Namespace:
parser = argparse.ArgumentParser(description=__doc__)
parser.add_argument("family", choices=sorted(FAMILY_BUILDERS))
parser.add_argument("n_min", type=int, nargs="?", default=1)
parser.add_argument("n_max", type=int, nargs="?", default=6)
parser.add_argument(
"--sources",
choices=("vertex", "cycle", "all"),
default="vertex",
help="candidate source family to search",
)
parser.add_argument(
"--quantifier",
choices=("exists-source", "all-sources"),
default="exists-source",
help="whether to test the weakened or stronger conjecture",
)
parser.add_argument(
"--max-cycle-source-size",
type=int,
default=None,
help="optional cap on induced cycle source size",
)
parser.add_argument(
"--max-colorings",
type=int,
default=None,
help="optional cap per graph/source; capped searches report UNKNOWN",
)
parser.add_argument(
"--full",
action="store_true",
help="continue after failures/unknowns instead of stopping at first",
)
return parser.parse_args()
def main() -> int:
args = parse_args()
builder = FAMILY_BUILDERS[args.family]
stop_first = not args.full
total_graphs = 0
total_sources = 0
unknown = 0
for n in range(args.n_min, args.n_max + 1):
g = builder(n)
total_graphs += 1
print(
f"{args.family} n={n}: "
f"|V|={g.n_vertices()} |E|={g.num_edges()} "
f"sources={args.sources} quantifier={args.quantifier}"
)
sources = list(
level_sources(g, args.sources, args.max_cycle_source_size)
)
passed, complete, checked_sources = test_graph(
g,
sources,
args.max_colorings,
stop_first,
args.quantifier,
)
total_sources += checked_sources
if not complete:
unknown += 1
if not passed and not args.full:
print(f"ABORT: first failure at family={args.family} n={n}")
print(
f"SUMMARY: checked {total_graphs} graphs and {total_sources} "
f"sources; unknown_graphs={unknown}"
)
return 1
print(
f"SUMMARY: checked {total_graphs} graphs and {total_sources} "
f"sources; unknown_graphs={unknown}"
)
return 0
if __name__ == "__main__":
logging.basicConfig(level=logging.INFO, format="%(levelname)s: %(message)s")
try:
raise SystemExit(main())
except Exception as exc: # pragma: no cover - surfaced to the shell
LOGGER.exception("candidate family generation failed: %s", exc)
raise
@@ -0,0 +1,291 @@
"""Kempe-class enumeration for vertex 4-colorings of tires.
For each tire T = (B_out, O, E_ann), we:
1. enumerate every proper vertex 4-coloring of V(T);
2. quotient by S_4 (color relabeling) via a first-appearance canonical
form, giving the set Q of canonical colorings;
3. build the *Kempe graph* on Q: for every canonical c in Q, every
color pair {a,b} in {0,1,2,3}, and every connected component K of
the subgraph of T induced by vertices colored a or b, swap
a <-> b on K, canonicalize the result, and add an edge;
4. count connected components of the Kempe graph.
A tire is *single-class* if its Kempe graph has one component, i.e. all
S_4-classes of 4-colorings are mutually Kempe-reachable.
The tire family enumerated is the (m, k, chord-set, lattice-path)
parameterization from the companion `coloring_nested_tire_dual_graphs`
paper: outer cycle on m vertices, inner cycle on k vertices with
non-crossing chords inside, annulus triangulated by a lattice path
(m 'O' moves, k 'I' moves) anchored at the spoke outer[0]-inner[0].
Note: distinct lattice paths can yield isomorphic tires, so the counts
here are over labeled-tire combinatorial classes, not isomorphism types.
Run:
python3 kempe_classes.py # default m,k<=5, no chords
python3 kempe_classes.py --m-max 6 --k-max 6 --max-chords 1
python3 kempe_classes.py --m 5 --k 4 --path OIOIOIOI --chords '' --dump
"""
from __future__ import annotations
import argparse
from collections import defaultdict, deque
from itertools import combinations
import time
def all_lattice_paths(m, k):
n = m + k
paths = []
def rec(prefix, o_left, i_left):
if o_left == 0 and i_left == 0:
paths.append(prefix)
return
if o_left:
rec(prefix + 'O', o_left - 1, i_left)
if i_left:
rec(prefix + 'I', o_left, i_left - 1)
rec('', m, k)
return paths
def chord_crosses(c1, c2):
a, b = c1; c, d = c2
return (a < c < b < d) or (c < a < d < b)
def all_noncrossing_chord_sets(k, max_chords):
candidates = [(a, b) for a in range(k) for b in range(a + 2, k)
if not (a == 0 and b == k - 1)]
out = [()]
def rec(start, chosen):
if len(chosen) >= max_chords:
return
for idx in range(start, len(candidates)):
ch = candidates[idx]
if any(chord_crosses(ch, old) for old in chosen):
continue
nxt = chosen + (ch,)
out.append(nxt)
rec(idx + 1, nxt)
rec(0, ())
return out
def build_tire(m, k, chords, lattice_path):
outer = list(range(m))
inner = list(range(m, m + k))
adj = [set() for _ in range(m + k)]
def add(u, v):
if u != v:
adj[u].add(v); adj[v].add(u)
for i in range(m):
add(outer[i], outer[(i + 1) % m])
for j in range(k):
add(inner[j], inner[(j + 1) % k])
for (a, b) in chords:
add(inner[a], inner[b])
add(outer[0], inner[0])
i, j = 0, 0
for mv in lattice_path:
if mv == 'O':
add(inner[j % k], outer[(i + 1) % m])
i += 1
else:
add(outer[i % m], inner[(j + 1) % k])
j += 1
return [tuple(sorted(s)) for s in adj]
def proper_4colorings(adj):
n = len(adj)
colors = [-1] * n
out = []
def rec(v):
if v == n:
out.append(tuple(colors))
return
used = 0
for u in adj[v]:
if u < v:
used |= 1 << colors[u]
for c in range(4):
if used & (1 << c):
continue
colors[v] = c
rec(v + 1)
colors[v] = -1
rec(0)
return out
def canonicalize(coloring):
mapping = {}
out = []
for c in coloring:
if c not in mapping:
mapping[c] = len(mapping)
out.append(mapping[c])
return tuple(out)
def kempe_neighbors(coloring, adj, a, b):
n = len(coloring)
in_set = [coloring[v] == a or coloring[v] == b for v in range(n)]
seen = [False] * n
out = []
for start in range(n):
if not in_set[start] or seen[start]:
continue
comp = []
q = deque([start])
seen[start] = True
while q:
v = q.popleft()
comp.append(v)
for u in adj[v]:
if in_set[u] and not seen[u]:
seen[u] = True
q.append(u)
new = list(coloring)
for v in comp:
new[v] = b if new[v] == a else a
out.append(tuple(new))
return out
def kempe_components(adj):
raw = proper_4colorings(adj)
canon = sorted({canonicalize(c) for c in raw})
index = {c: i for i, c in enumerate(canon)}
parent = list(range(len(canon)))
def find(x):
while parent[x] != x:
parent[x] = parent[parent[x]]
x = parent[x]
return x
def union(x, y):
rx, ry = find(x), find(y)
if rx != ry:
parent[rx] = ry
for c in canon:
ci = index[c]
for a, b in combinations(range(4), 2):
for swapped in kempe_neighbors(c, adj, a, b):
cs = canonicalize(swapped)
if cs == c:
continue
union(ci, index[cs])
classes = defaultdict(list)
for c, ci in index.items():
classes[find(ci)].append(c)
return list(classes.values()), len(raw)
def format_chords(chords):
return ','.join(f'{a}-{b}' for a, b in chords) if chords else 'none'
def sweep(m_max, k_max, max_chords, verbose=False):
multi = []
rows = []
t0 = time.time()
for m in range(3, m_max + 1):
for k in range(3, k_max + 1):
chord_sets = all_noncrossing_chord_sets(k, max_chords)
paths = all_lattice_paths(m, k)
n_tires = len(chord_sets) * len(paths)
t_mk = time.time()
for chords in chord_sets:
for path in paths:
adj = build_tire(m, k, chords, path)
classes, n_raw = kempe_components(adj)
n_classes = len(classes)
n_canon = sum(len(cl) for cl in classes)
rows.append((m, k, chords, path, n_raw, n_canon, n_classes))
if n_classes > 1:
multi.append((m, k, chords, path, n_raw, n_canon,
n_classes, classes))
if verbose:
print(f" m={m} k={k}: {n_tires} tires in "
f"{time.time() - t_mk:.2f}s")
elapsed = time.time() - t0
return rows, multi, elapsed
def print_summary(rows, multi, elapsed):
by_count = defaultdict(int)
for r in rows:
by_count[r[6]] += 1
print(f"# tires checked: {len(rows)} in {elapsed:.2f}s")
print("Kempe class count distribution:")
for nc, cnt in sorted(by_count.items()):
print(f" {nc} class(es): {cnt} tires")
print(f"# multi-class tires: {len(multi)}")
if multi:
by_mk = defaultdict(int)
for (m, k, *_rest) in multi:
by_mk[(m, k)] += 1
print("multi-class breakdown by (m, k):")
for (m, k), cnt in sorted(by_mk.items()):
print(f" (m={m}, k={k}): {cnt}")
def dump_multi(multi, limit=10, show_classes=False):
if not multi:
return
print()
print(f"first {min(limit, len(multi))} multi-class tires:")
for (m, k, chords, path, n_raw, n_canon, n_classes, classes) in multi[:limit]:
print(f" m={m} k={k} chords={format_chords(chords)} path={path}: "
f"raw={n_raw} canon={n_canon} classes={n_classes}")
if show_classes:
for i, cl in enumerate(classes):
rep = sorted(cl)[0]
print(f" class {i} (size {len(cl)}): rep={rep}")
def main():
parser = argparse.ArgumentParser(description=__doc__)
parser.add_argument('--m', type=int, help='single tire: outer length')
parser.add_argument('--k', type=int, help='single tire: inner length')
parser.add_argument('--path', type=str, help='single tire: lattice path')
parser.add_argument('--chords', type=str, default='',
help='single tire: e.g. "0-2,1-3" or empty')
parser.add_argument('--m-max', type=int, default=5)
parser.add_argument('--k-max', type=int, default=5)
parser.add_argument('--max-chords', type=int, default=0)
parser.add_argument('--show-multi', type=int, default=10,
help='print up to N multi-class tires (default 10)')
parser.add_argument('--dump', action='store_true',
help='print full class data for each multi-class tire')
parser.add_argument('-v', '--verbose', action='store_true')
args = parser.parse_args()
if args.m is not None and args.k is not None and args.path is not None:
chords = ()
if args.chords:
chords = tuple(tuple(sorted((int(a), int(b))))
for a, b in (p.split('-') for p in args.chords.split(',')))
adj = build_tire(args.m, args.k, chords, args.path)
classes, n_raw = kempe_components(adj)
n_classes = len(classes)
n_canon = sum(len(cl) for cl in classes)
print(f"m={args.m} k={args.k} chords={format_chords(chords)} "
f"path={args.path}")
print(f" raw 4-colorings: {n_raw}")
print(f" canonical (mod S_4): {n_canon}")
print(f" Kempe classes: {n_classes}")
for i, cl in enumerate(classes):
rep = sorted(cl)[0]
print(f" class {i}: size={len(cl)} rep={rep}")
return
rows, multi, elapsed = sweep(args.m_max, args.k_max, args.max_chords,
verbose=args.verbose)
print_summary(rows, multi, elapsed)
dump_multi(multi, limit=args.show_multi, show_classes=args.dump)
if __name__ == '__main__':
main()
@@ -0,0 +1,462 @@
"""Support on genuine level-cycle candidates inside a tire.
Here a tested cycle is not an arbitrary tire boundary. It must be a
bounded face cycle of the inner outerplanar graph O, distinct from
O's outer-face boundary. This models a level/seam cycle as it appears
inside the parent's next-level graph, rather than treating it as an
outer boundary of a tire at the same level.
For each such cycle C, the support is the set of proper 4-colorings of
C that extend to a proper 4-coloring of the parent tire graph.
"""
from __future__ import annotations
import argparse
from functools import lru_cache
from itertools import combinations, permutations, product
from math import comb
COLORS = (0, 1, 2, 3)
def canonical_edge(u: int, v: int) -> tuple[int, int]:
return (u, v) if u < v else (v, u)
def cycle_edges(vertices: list[int]) -> set[tuple[int, int]]:
return {
canonical_edge(vertices[i], vertices[(i + 1) % len(vertices)])
for i in range(len(vertices))
}
def chord_crosses(c1: tuple[int, int], c2: tuple[int, int]) -> bool:
a, b = sorted(c1)
c, d = sorted(c2)
return (a < c < b < d) or (c < a < d < b)
def noncrossing_chord_sets(k: int, max_chords: int | None = None):
candidates = [
(a, b)
for a in range(k)
for b in range(a + 2, k)
if not (a == 0 and b == k - 1)
]
out = [()]
def rec(start: int, chosen: tuple[tuple[int, int], ...]) -> None:
if max_chords is not None and len(chosen) >= max_chords:
return
for idx in range(start, len(candidates)):
ch = candidates[idx]
if any(chord_crosses(ch, old) for old in chosen):
continue
nxt = chosen + (ch,)
out.append(nxt)
rec(idx + 1, nxt)
rec(0, ())
return tuple(sorted(set(out), key=lambda cs: (len(cs), cs)))
def lattice_paths(m: int, k: int):
n = m + k
for outer_positions in combinations(range(n), m):
outer_positions = set(outer_positions)
yield "".join("O" if i in outer_positions else "I" for i in range(n))
def tire_edges(m: int, k: int, path: str, chords: tuple[tuple[int, int], ...]) -> tuple[tuple[int, int], ...]:
outer = list(range(m))
inner = list(range(m, m + k))
edges = set()
edges |= cycle_edges(outer)
edges |= cycle_edges(inner)
for a, b in chords:
edges.add(canonical_edge(inner[a], inner[b]))
edges.add(canonical_edge(outer[0], inner[0]))
i = j = 0
for move in path:
if move == "O":
edges.add(canonical_edge(outer[(i + 1) % m], inner[j % k]))
i += 1
else:
edges.add(canonical_edge(outer[i % m], inner[(j + 1) % k]))
j += 1
return tuple(sorted(edges))
def proper_cycle_colorings(n: int) -> tuple[tuple[int, ...], ...]:
out = []
for colors in product(COLORS, repeat=n):
if all(colors[i] != colors[(i + 1) % n] for i in range(n)):
out.append(colors)
return tuple(out)
@lru_cache(maxsize=None)
def boundary_support(
n_vertices: int,
edges: tuple[tuple[int, int], ...],
boundary_vertices: tuple[int, ...],
) -> frozenset[tuple[int, ...]]:
assigned = {0: 0}
adj = {v: set() for v in range(n_vertices)}
for u, v in edges:
adj[u].add(v)
adj[v].add(u)
remaining = [v for v in range(n_vertices) if v not in assigned]
remaining.sort(key=lambda v: (-len(adj[v]), v))
support = set()
def dfs(index: int) -> None:
if index == len(remaining):
support.add(tuple(assigned[v] for v in boundary_vertices))
return
best_at = index
best_options = None
for pos in range(index, len(remaining)):
v = remaining[pos]
used = {assigned[w] for w in adj[v] if w in assigned}
options = tuple(c for c in COLORS if c not in used)
if best_options is None or len(options) < len(best_options):
best_at = pos
best_options = options
if len(options) <= 1:
break
if not best_options:
return
remaining[index], remaining[best_at] = remaining[best_at], remaining[index]
v = remaining[index]
for color in best_options:
assigned[v] = color
dfs(index + 1)
assigned.pop(v)
remaining[index], remaining[best_at] = remaining[best_at], remaining[index]
dfs(0)
return frozenset(support)
def rotate_tuple(values: tuple[int, ...], shift: int) -> tuple[int, ...]:
n = len(values)
return tuple(values[(i + shift) % n] for i in range(n))
def normalize_support(support: frozenset[tuple[int, ...]]) -> frozenset[tuple[int, ...]]:
out = set()
for state in support:
for perm in permutations(COLORS):
relabeled = tuple(perm[c] for c in state)
for seq in (relabeled, relabeled[::-1]):
for shift in range(len(seq)):
out.add(rotate_tuple(seq, shift))
return frozenset(out)
def describe_chords(chords: tuple[tuple[int, int], ...]) -> str:
return ",".join(f"{a}-{b}" for a, b in chords) if chords else "none"
def canonicalize_tire_cycle(
m: int,
k: int,
path: str,
chords: tuple[tuple[int, int], ...],
cycle: tuple[int, ...],
) -> tuple[str, tuple[tuple[int, int], ...], tuple[int, ...]]:
"""Canonical form of (tire, level cycle) under tire symmetries.
The tire has dihedral symmetry of order 2(m+k) on the rung sequence:
cyclic shift s = "start at rung s of the original path", and reflection
= "traverse in reverse" (the path string reverses, inner cycle direction
flips so chord (a,b) becomes ((k-a) mod k, (k-b) mod k)).
The level cycle is transported by the same rigid relabelling and then
normalized under its own D_n (the support is invariant under D_n on the
cycle's vertex sequence, so this stage is part of the canonical form).
"""
n_rung = m + k
n_cycle = len(cycle)
best = None
for reverse in (False, True):
if reverse:
p_base = path[::-1]
cs_base = tuple(
canonical_edge((k - a) % k, (k - b) % k) for a, b in chords
)
c_base = tuple((k - v) % k for v in reversed(cycle))
else:
p_base = path
cs_base = chords
c_base = cycle
prefix_i = [0]
for ch in p_base:
prefix_i.append(prefix_i[-1] + (1 if ch == "I" else 0))
for s in range(n_rung):
b_s = prefix_i[s]
shifted = p_base[s:] + p_base[:s]
new_cs = tuple(
sorted(
canonical_edge((a - b_s) % k, (b - b_s) % k)
for a, b in cs_base
)
)
new_c = tuple((v - b_s) % k for v in c_base)
norm_c = min(
tuple(orient[(r + i) % n_cycle] for i in range(n_cycle))
for orient in (new_c, new_c[::-1])
for r in range(n_cycle)
)
cand = (shifted, new_cs, norm_c)
if best is None or cand < best:
best = cand
return best
def interval_vertices(vertices: tuple[int, ...], a: int, b: int) -> tuple[int, ...]:
ia = vertices.index(a)
out = [a]
i = ia
while vertices[i] != b:
i = (i + 1) % len(vertices)
out.append(vertices[i])
return tuple(out)
def chord_inside(poly: tuple[int, ...], chord: tuple[int, int]) -> bool:
a, b = chord
return a in poly and b in poly
def polygon_faces(poly: tuple[int, ...], chords: tuple[tuple[int, int], ...]) -> list[tuple[int, ...]]:
"""Cells inside a polygon cut by noncrossing chords."""
usable = [ch for ch in chords if chord_inside(poly, ch)]
split = None
for a, b in usable:
if a not in poly or b not in poly:
continue
ia, ib = poly.index(a), poly.index(b)
distance = abs(ia - ib)
if distance in (1, len(poly) - 1):
continue
split = (a, b)
break
if split is None:
return [poly]
a, b = split
side1 = interval_vertices(poly, a, b)
side2 = interval_vertices(poly, b, a)
rest = tuple(ch for ch in usable if ch != split)
return polygon_faces(side1, rest) + polygon_faces(side2, rest)
def level_cycles_in_o(k: int, chords: tuple[tuple[int, int], ...]) -> tuple[tuple[int, ...], ...]:
"""Bounded face cycles of O that are not the outer boundary of O."""
if not chords:
return ()
outer = tuple(range(k))
faces = polygon_faces(outer, chords)
out = []
for face in faces:
if len(face) == k and set(face) == set(outer):
continue
out.append(face)
return tuple(out)
def enumerate_level_cycle_supports(
n: int,
outer_min: int,
outer_max: int,
inner_min: int,
inner_max: int,
max_chords: int | None,
max_paths: int | None,
canonicalize: bool = True,
progress: bool = False,
) -> tuple[dict[frozenset[tuple[int, ...]], list[dict]], dict]:
supports: dict[frozenset[tuple[int, ...]], list[dict]] = {}
seen_canon: set = set()
stats = {"raw": 0, "canonical": 0}
for m in range(outer_min, outer_max + 1):
for k in range(max(inner_min, n), inner_max + 1):
for chords in noncrossing_chord_sets(k, max_chords):
level_cycles = [cycle for cycle in level_cycles_in_o(k, chords) if len(cycle) == n]
if not level_cycles:
continue
for path_idx, path in enumerate(lattice_paths(m, k)):
if max_paths is not None and path_idx >= max_paths:
break
edges = None
for cycle in level_cycles:
stats["raw"] += 1
if canonicalize:
canon = canonicalize_tire_cycle(m, k, path, chords, cycle)
if canon in seen_canon:
continue
seen_canon.add(canon)
stats["canonical"] += 1
if edges is None:
edges = tire_edges(m, k, path, chords)
boundary = tuple(m + v for v in cycle)
support = normalize_support(boundary_support(m + k, edges, boundary))
meta = {
"m": m,
"k": k,
"path": path,
"chords": chords,
"cycle": cycle,
}
supports.setdefault(support, []).append(meta)
if progress:
print(
f" m={m} k={k} chords={describe_chords(chords)} "
f"raw={stats['raw']} canonical={stats['canonical']} "
f"supports={len(supports)}",
flush=True,
)
return supports, stats
def check_floor_containment(
supports: dict[frozenset[tuple[int, ...]], list[dict]],
) -> None:
"""Test whether the smallest-size support is a subset of every other support.
The supports are fully normalized (orbits under S_4 x D_n), so set
inclusion here is the right test for the "floor support is contained in
every admissible support" conjecture.
"""
if len(supports) < 2:
print(" containment: <2 supports, trivially contained")
return
keys = list(supports.keys())
min_size = min(len(k) for k in keys)
floors = [k for k in keys if len(k) == min_size]
print(f" containment check: floor support (size {min_size}) vs {len(keys) - 1} others")
for floor in floors:
bad: list[tuple[int, tuple[int, ...]]] = []
for other in keys:
if other is floor:
continue
if not floor.issubset(other):
missing = next(iter(floor - other))
bad.append((len(other), missing))
if not bad:
print(f" floor IS a subset of all {len(keys) - 1} other supports")
else:
print(f" floor is NOT a subset of {len(bad)} of {len(keys) - 1} other supports")
for size, missing in bad[:5]:
print(f" missing example: floor coloring {missing} absent from support of size {size}")
def summarize(
n: int,
supports: dict[frozenset[tuple[int, ...]], list[dict]],
examples: int,
stats: dict | None = None,
) -> None:
all_colorings = len(proper_cycle_colorings(n))
if not supports:
print()
print(f"n={n}: no admissible level-cycle candidates in search window")
return
min_size = min(len(support) for support in supports)
max_size = max(len(support) for support in supports)
min_supports = [support for support in supports if len(support) == min_size]
pair_overlaps = [
len(a & b)
for i, a in enumerate(min_supports)
for b in min_supports[i:]
]
print()
print(f"n={n}")
if stats:
print(f" raw (tire,cycle) combos : {stats['raw']}")
print(f" canonical (tire,cycle) classes: {stats['canonical']}")
print(f" proper C_n colorings : {all_colorings}")
print(f" distinct level-cycle supports : {len(supports)}")
print(f" most restrictive support : {min_size}/{all_colorings} ({len(min_supports)} support types)")
print(f" least restrictive support : {max_size}/{all_colorings}")
print(f" overlap among max-restrict : min {min(pair_overlaps)}, max {max(pair_overlaps)}")
check_floor_containment(supports)
print(" examples:")
printed = 0
for support, metas in sorted(supports.items(), key=lambda item: (len(item[0]), len(item[1]))):
if len(support) != min_size:
continue
for meta in metas[:examples]:
print(
f" size={len(support)} m={meta['m']} k={meta['k']} "
f"path={meta['path']} chords={describe_chords(meta['chords'])} "
f"cycle={meta['cycle']}"
)
printed += 1
if printed >= examples:
return
def main() -> None:
parser = argparse.ArgumentParser(description=__doc__)
parser.add_argument("--n-min", type=int, default=3)
parser.add_argument("--n-max", type=int, default=7)
parser.add_argument("--outer-min", type=int, default=3)
parser.add_argument("--outer-max", type=int, default=7)
parser.add_argument("--inner-min", type=int, default=3)
parser.add_argument("--inner-max", type=int, default=9)
parser.add_argument("--max-chords", type=int, default=None)
parser.add_argument("--max-paths", type=int, default=None)
parser.add_argument("--examples", type=int, default=4)
parser.add_argument(
"--no-canonicalize",
action="store_true",
help="disable tire automorphism deduplication",
)
parser.add_argument(
"--progress",
action="store_true",
help="emit a one-line update after each (m, k, chord set)",
)
args = parser.parse_args()
print("Level-cycle support inside parent tire inner graph O")
print(" tested cycles: bounded face cycles of O, excluding O's outer boundary")
print(f" outer length range : {args.outer_min}..{args.outer_max}")
print(f" inner O size range : {args.inner_min}..{args.inner_max}")
print(f" max chords : {args.max_chords if args.max_chords is not None else 'all'}")
print(f" max paths/type : {args.max_paths if args.max_paths is not None else 'all'}")
for n in range(args.n_min, args.n_max + 1):
rough_paths = sum(
comb(m + k, m)
for m in range(args.outer_min, args.outer_max + 1)
for k in range(max(args.inner_min, n), args.inner_max + 1)
)
print(f"computing n={n} (rough path count before chords: {rough_paths})")
supports, stats = enumerate_level_cycle_supports(
n,
args.outer_min,
args.outer_max,
args.inner_min,
args.inner_max,
args.max_chords,
args.max_paths,
canonicalize=not args.no_canonicalize,
progress=args.progress,
)
summarize(n, supports, args.examples, stats)
if __name__ == "__main__":
main()
@@ -0,0 +1,311 @@
# Level-Cycle Support Findings
This is the corrected version of the boundary-overlap test.
The key modeling change is that a tested cycle must appear in the
level-cycle/seam role: as a bounded face cycle inside the parent
tire's inner outerplanar graph `O`, not as an arbitrary `B_out` or as
the outer-face boundary of `O`.
Executable:
```bash
python3 papers/nested_tire_decompositions_of_plane_triangulations/experiments/level_cycle_support.py
```
## Model
For a parent tire `T = (B_out, O, E_ann)`, enumerate simple bounded
face cycles of `O`.
A cycle is admissible only if:
- it is a bounded face cycle of `O`;
- it is distinct from the outer-face boundary of `O`;
- it is tested in this inner/next-level role, never as an outer
boundary of a tire at the same level.
For each admissible cycle `C`, compute the set of proper 4-colorings
of `C` that extend to a proper 4-coloring of the parent tire graph.
Supports are normalized under color relabeling and dihedral symmetries
of `C`.
## Capped Validation Run
Command:
```bash
python3 -u papers/nested_tire_decompositions_of_plane_triangulations/experiments/level_cycle_support.py \
--n-min 3 --n-max 6 --outer-max 5 --inner-max 7 --max-chords 2 --max-paths 30
```
Result:
```text
n=3
proper C_n colorings : 24
distinct level-cycle supports : 1
most restrictive support : 24/24
overlap among max-restrict : 24
n=4
proper C_n colorings : 84
distinct level-cycle supports : 3
most restrictive support : 60/84
overlap among max-restrict : 60
n=5
proper C_n colorings : 240
distinct level-cycle supports : 2
most restrictive support : 120/240
overlap among max-restrict : 120
n=6
proper C_n colorings : 732
distinct level-cycle supports : 13
most restrictive support : 252/732
overlap among max-restrict : 252
```
The most restrictive admissible `n=4` level-cycle support found here
has size `60/84`, and there is only one worst support type in this
capped window.
Representative `n=4` admissible witness:
```text
size=60
m=3, k=5
path=OOOIIIII
chords=0-2
cycle=(2, 3, 4, 0)
```
Here `O` is a 5-cycle with chord `0-2`. The tested 4-cycle is the
bounded face cycle `(2,3,4,0)`, not the outer-face boundary of `O`.
## Current Interpretation
With level-cycle admissibility enforced, the first-pass data no longer
supports a zero-overlap obstruction at `n=4`. In the capped search,
the maximum-restriction support type is unique for `n=3,4,5,6`, so
overlap among maximum restrictions is trivially the whole worst
support.
This is not yet a proof. The exact all-path `n=4` run with
`--max-chords 2` was stopped after it ran too long interactively. The
next implementation step should canonicalize outerplanar `O` and
annular paths, or switch to a transfer/DP support computation, before
claiming exhaustive results beyond small capped windows.
## Canonical Tire Quotient
The script now quotients out the dihedral symmetry of the tire on the
rung sequence. Concretely, a tire `T = (m, k, path, chords)` together
with a chosen level cycle `C` admits an order-`2(m+k)` action:
- cyclic shift `s`: "start counting from rung `s` of the original path".
This rotates the inner labelling by `-b_s mod k`, where `b_s` is the
number of inner steps in the first `s` moves; chords and `C` are
carried by the same shift.
- reflection: traverse the tire in the opposite direction. The path
string reverses and each inner label `j` flips to `(k - j) mod k`,
taking chord `(a, b)` to `((k - a) mod k, (k - b) mod k)` and reversing
`C`.
The canonical form of `(T, C)` is the lex-min `(path, chords, cycle)`
under that action, with `C` itself further minimised under its own
`D_n` (which the support already quotients out, so this stage is free).
Two `(T, C)` pairs in the same canonical class produce identical
normalised supports, so we compute the support once per class. Sanity
checks at `n = 3, 4, 5` reproduce the prior capped support sizes
(`24/24`, `60/84`, `120/240`) exactly while reducing raw work by
roughly 20×–25×.
## Exhaustive `n=6` Run
With the canonical quotient in place we can now exhaust a meaningful
window for `n = 6`. The smallest admissible inner ring is `k = 7`
(a `k`-cycle plus chords cannot host a non-outer bounded `6`-face for
`k < 7`).
Command:
```bash
python3 -u papers/nested_tire_decompositions_of_plane_triangulations/experiments/level_cycle_support.py \
--n-min 6 --n-max 6 --outer-min 3 --outer-max 6 --inner-min 7 --inner-max 8 \
--progress --examples 6
```
Result:
```text
n=6
raw (tire,cycle) combos : 238506
canonical (tire,cycle) classes: 9144
proper C_6 colorings : 732
distinct level-cycle supports : 17
most restrictive support : 252/732 (1 support type)
least restrictive support : 732/732
overlap among max-restrict : 252
```
Compared to the earlier `--outer-max 5 --inner-max 7 --max-chords 2
--max-paths 30` capped run, the distinct-support count climbs from
`13` to `17`, but the **minimum support size is unchanged at `252/732`
and is still realised by a unique support type**. The minimum is
witnessed by the same minimal-`O` configuration that already showed up
at smaller `n`:
```text
size=252
m=3, k=7
chords=0-2
cycle=(2, 3, 4, 5, 6, 0)
```
i.e. the bounded `6`-face of a `7`-cycle with one chord, sitting inside
the thinnest annulus `(m=3)`. Adding outer length (`m` up to `6`),
inner length (`k` up to `8`), and unrestricted chord sets produces
strictly *less* restrictive supports — never a new floor.
### Wider sweep: `outer 3..7, inner 7..9`
Command:
```bash
python3 -u papers/nested_tire_decompositions_of_plane_triangulations/experiments/level_cycle_support.py \
--n-min 6 --n-max 6 --outer-min 3 --outer-max 7 --inner-min 7 --inner-max 9 \
--progress --examples 6
```
Result:
```text
n=6
raw (tire,cycle) combos : 5662518
canonical (tire,cycle) classes: 186818
proper C_6 colorings : 732
distinct level-cycle supports : 19
most restrictive support : 252/732 (1 support type)
least restrictive support : 732/732
overlap among max-restrict : 252
```
Adding `k = 9` and `m = 7` brings 2 new distinct supports (`17 → 19`),
**both strictly above the floor**. The most restrictive support is
**still `252/732`, still unique, and still realised by the same
minimal-`O` witness** (`m=3, k=7, chord=0-2, cycle=(2,3,4,5,6,0)`).
The `m = 3` configurations dominated the floor in every (`m`, `k`)
sweep examined.
### What this changes
- The "most restrictive support is unique" claim for `n = 6` is now
backed by an exhaustive (not capped) sweep over `m ∈ [3, 7]`,
`k ∈ [7, 9]`, all chord sets, all annular paths.
- The earlier-feared zero-overlap obstruction at `n = 4` does not
reappear at `n = 6` either: overlap among maximum-restriction
supports is trivially the whole worst support, because there is only
one worst support.
- The witness for the floor is structurally the same across
`n = 3, 4, 5, 6`: a single chord on a `(n+1)`-cycle, embedded in the
thinnest annulus, with the tested cycle taken as the bounded
`n`-face. That stability is suggestive (it hints that the worst
level-cycle support is governed by a small canonical configuration)
but is not yet a theorem.
### Floor-stability-in-`m` conjecture
Across every searched `n`, the floor witness has been `m = 3`. This
is consistent with a **support-monotonicity** picture: subdividing any
outer or annular edge of an `m = 3` floor witness produces an `m = 4`
tire whose support strictly contains the original (the new degree-`2`
vertex adds coloring freedom, and the subdivided edge's endpoints are
no longer adjacent, so they may share a color). By induction the
floor over `m ≥ 3` is bounded above by the `m = 3` floor.
The empirical run confirms this bound is tight up to `m ≤ 7, k ≤ 9` at
`n = 6`: no `m ≥ 4` tire produced a support strictly smaller than the
`m = 3` floor. A theorem-style statement would be:
> **(Conjecture)** For every `n`, every `k ≥ n + 1`, and every chord
> set on `C_k` containing an `n`-face, the level-cycle support floor
> over all annular paths and all `m ≥ 3` is achieved at `m = 3`.
If true, this collapses the exhaustive search to `m = 3` only and
opens the door to closed-form support computation for the worst case.
The obstruction to a quick proof is exotic `m ≥ 4` configurations not
reachable by subdivision from an `m = 3` floor witness — none has
appeared empirically, but their non-existence is not yet ruled out.
#### Skip-`m=3` sweep (partial)
To probe the conjecture more directly we ran a "skip-`m=3`" sweep
explicitly excluding `m = 3` from the search:
```bash
python3 -u papers/nested_tire_decompositions_of_plane_triangulations/experiments/level_cycle_support.py \
--n-min 6 --n-max 6 --outer-min 4 --outer-max 10 --inner-min 7 --inner-max 9 \
--progress
```
The sweep ran for `11h 49m` and was terminated partway through `m = 8,
k = 9` at chord-set #6 of the 2-chord block (raw=6.45M canonical=223k).
Throughout the run --- across `m ∈ [4, 7]` exhaustively and `m = 8`
partially --- the distinct-support count stayed locked at **`13`**
(vs `19` for the full `m ∈ [3, 7]` run). The six missing support
types are precisely the ones with `m = 3`-only witnesses, including
the unique `252/732` floor.
Conclusion of the partial run: no support of size `≤ 252` appeared
under `m ≥ 4` in any configuration searched, and the support count
saturated early, suggesting the support landscape for `m ≥ 4` is
strictly looser than for `m = 3` even as `m` grows. The conjecture is
not falsified by any data we have; pushing `m` to `9` or `10` is
left as future work (path-count growth makes it expensive: `m = 10,
k = 9` alone has `C(19, 10) ≈ 92{,}000` paths per chord set).
### Floor-containment conjecture — refuted
Floor-stability bounds the *size* of the worst-case support but not
its content. For the tire-tree compatibility argument, what would
have closed the loop is a containment statement:
> **(Conjecture, refuted)** For every `n`, the unique floor support
> `F_n` is a *subset* of every admissible level-cycle support. Every
> level-cycle coloring that the `m = 3` floor witness allows is also
> allowed by every other tire.
The `check_floor_containment` helper in `level_cycle_support.py`
tests this directly on the computed supports. The conjecture **fails
at `n = 4` and `n = 6`**:
```text
n=4: floor (size 60) is NOT a subset of 1 of 2 other supports
missing: floor coloring (1, 2, 1, 2) absent from support of size 72
n=6: floor (size 252) is NOT a subset of 11 of 16 other supports
missing: floor coloring (1, 3, 2, 1, 3, 2) absent from support of size 708
missing: floor coloring (2, 3, 2, 1, 3, 1) absent from support of size 492
missing: floor coloring (2, 3, 2, 3, 2, 3) absent from support of size 720
```
(`n = 3` is trivial — only one support type. `n = 5` happens to
satisfy containment in the searched window but only against a single
other support, so the data is too thin to be evidence either way.)
The missing colorings cluster on **bipartite alternations**
(`(1,2,1,2)`, `(2,3,2,3,2,3)`) and **3-periodic patterns**
(`(1,3,2,1,3,2)`). These are the most "structured" colorings of `C_n`
— colorings the thin `m = 3` annulus is free to produce, but other
tires (with larger annulus / heavier chord patterns) actively forbid
because their interior forces additional colour variety.
**Consequence.** The simple structural shortcut — "all supports
contain a common floor, hence pairwise intersections are trivially
non-empty" — does not hold. Same-`n` compatibility (which by `4CT` is
still forced to hold) cannot be reduced to a single containment fact;
it requires a finer structural analysis of *which* colorings sit in
*which* supports, or a different shortcut entirely.