Add planar counterexample figure

papers/coloring_nested_tire_graphs/experiments/draw_universal_level_cycle_counterexample.py

@@ -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())

papers/coloring_nested_tire_graphs/experiments/generate_candidate_families.py

@@ -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

papers/coloring_nested_tire_graphs/paper.tex

@@ -1298,6 +1298,15 @@ level source.  Then $G$ admits a proper $4$-vertex-colouring with the
 level-cycle three-colour restriction with respect to $S$.
 \end{conjecture}
 
+\begin{figure}[htbp]
+\centering
+\includegraphics[width=0.78\textwidth]{fig_universal_level_cycle_counterexample.png}
+\caption{The $8$-vertex counterexample to the universal-source form.
+With source $S=\{7\}$, the level cycle $(3,4,5,8)$ lies in $L_2$ and
+forces all four colours in every proper $4$-vertex-colouring.}
+\label{fig:universal-level-cycle-counterexample}
+\end{figure}
+
 \begin{example}[Counterexample to Conjecture~\ref{conj:false-universal-level-cycle-three-colour}]
 \label{ex:universal-level-cycle-counterexample}
 Let $G$ be the maximal planar graph on vertex set