Adds search_counterexample_comprehensive iterating Sage's planar_graphs
generator across all maximal planar graphs of bounded order. Exhaustive
enumeration through order 13 (9150+49566 triangulations) yields exactly
one graph with no plane diamond coloring, at order 13. Updates Theorem
2.6 to assert minimality and uniqueness, and replaces the figure and
edge list with the smaller counterexample.
Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com>
Extends paper with: a notation section for color-class preimages; the
plane diamond coloring definition (4-coloring whose two classes lift to a
2-coloring of some BFS-rooted diamond scaffold); a connectedness lemma
for the scaffold; a proposition reformulating the property as parity-
separation of two color classes by BFS layers; a remark noting this is
strictly stronger than 4CT; and the conjecture that every maximal planar
graph admits such a coloring.
Adds plane_diamond_coloring.py with get_plane_diamond_scaffold and a
counterexample search that reduces the per-root check to 4-colorability
of an auxiliary graph forcing two colors onto opposite parity layers.
Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com>
didericis