face_monochromatic_pairs: strengthen Conj 5.5 to face-length ≥ 5, find 28-vertex counterexample

- Paper: Conjecture 5.5 restated with the hypothesis that every face
  of H has length ≥ 5 (= the cubic plane analogue of "no triangles
  or quadrilaterals as faces"). This kills K_4 and the n=8 trivial
  counterexamples (girth 3) and the ad-hoc n=40 counterexample
  (which has 2 triangles and 4 quadrilaterals). A new remark catalogues
  these excluded counterexamples and the smallest cubic plane graphs
  satisfying the hypothesis (dodecahedron at |V| = 20).
- search_smaller_counterexample.py: --min-face=N option to filter
  cubic planar graphs by minimum face length.
- search_min_face5_counterexample.py: enumerates triangulations T
  with min degree ≥ 5 via graphs.triangulations(n, minimum_degree=5),
  takes planar dual (= cubic plane with all faces ≥ 5), and runs the
  Heawood-constancy check.
- Result: smallest counterexample at triangulation order n_T = 16,
  whose dual is a 28-vertex cubic plane graph (graph6
  [kG[A?_A?_?_?K?D?@_CO?o?@_??A??@C??O??AG?C????`???a???W???A_???F).
  Faces: 12 pentagons + 4 hexagons (a C28 fullerene). Both
  K_{red, blue} and K_{red, green} are 12-cycles sharing the
  colour-red edge (0, 1) and both have h_φ ≡ -1. 8 of 28 vertices
  lie outside V(K_0) ∪ V(K_1).
- verify_28_vertex_counterexample.py: reproduces the counterexample,
  verifies all properties, and renders figures/min-face-5-counterexample.png.

Note on the boundary: face-length ≥ 6 is impossible for cubic plane
graphs by Euler (6F = 6(V/2 + 2) > 3V = sum face lengths for V > 4).
So face-length ≥ 5 is the strongest face-length restriction admitting
any cubic plane graphs at all.

Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com>
This commit is contained in:
2026-05-25 03:42:08 -04:00
parent 3aec31b3ac
commit 10a53e9de1
6 changed files with 342 additions and 53 deletions
@@ -0,0 +1,120 @@
"""Verify the n=28 counterexample (smallest dual of min-degree-5
triangulation that violates the face-length-≥-5 form of Conjecture
5.5) and render a planar PNG of it.
The graph H is the planar dual of a 16-vertex triangulation with
min degree ≥ 5 (the 3rd one in sage's enumeration). It has 28
vertices, 42 edges, and all faces of length ≥ 5. The colouring shown
below makes K_{red, blue} and K_{red, green} both 12-cycles sharing
the colour-red edge (0, 1) with h_φ ≡ -1 on each.
Run with: sage experiments/verify_28_vertex_counterexample.py
"""
import os
import sys
import math
from sage.all import Graph
HERE = os.path.dirname(os.path.abspath(__file__))
sys.path.insert(0, HERE)
from search_smaller_counterexample import (
edge_key, heawood_numbers, trace_kempe,
)
OUT_PNG = os.path.join(HERE, '..', 'figures', 'min-face-5-counterexample.png')
# Dual edges and the discovered colouring (sorted-edge order).
EDGES_LIST = [
(0, 1), (0, 4), (0, 6), (1, 2), (1, 5), (2, 3), (2, 8), (3, 4),
(3, 11), (4, 13), (5, 7), (5, 9), (6, 7), (6, 15), (7, 17),
(8, 10), (8, 12), (9, 10), (9, 19), (10, 20), (11, 12), (11, 14),
(12, 22), (13, 14), (13, 16), (14, 23), (15, 16), (15, 18),
(16, 25), (17, 18), (17, 19), (18, 26), (19, 21), (20, 21),
(20, 22), (21, 27), (22, 24), (23, 24), (23, 25), (24, 27),
(25, 26), (26, 27),
]
COLOURING = (0, 1, 2, 2, 1, 1, 0, 2, 0, 0, 2, 0, 1, 0, 0, 1, 2, 2,
1, 0, 1, 2, 0, 1, 2, 0, 1, 2, 0, 1, 2, 0, 0, 2, 1, 1,
2, 1, 2, 0, 1, 2)
COLOUR_NAME = {0: 'red', 1: 'blue', 2: 'green'}
def build():
G = Graph(multiedges=False, loops=False)
for u, v in EDGES_LIST:
G.add_edge(u, v)
# Sage's sorted edges should align with EDGES_LIST.
edges_sorted = sorted([edge_key(u, v) for (u, v) in G.edge_iterator(labels=False)])
assert edges_sorted == EDGES_LIST, "edge order mismatch"
col_of_edge = {edges_sorted[i]: COLOURING[i] for i in range(len(edges_sorted))}
return G, col_of_edge
def main():
G, col_of_edge = build()
print(f"|V| = {G.order()}, |E| = {G.size()}")
assert G.is_planar(set_embedding=True)
print(f"face lengths: {sorted([len(f) for f in G.faces()])}")
assert all(len(f) >= 5 for f in G.faces()), "face length < 5"
# Verify proper 3-edge-colouring.
for v in G.vertex_iterator():
cs = sorted(col_of_edge[edge_key(v, u)] for u in G.neighbors(v))
assert cs == [0, 1, 2], f"vertex {v} colours {cs}"
print("proper 3-edge-colouring ✓")
h = heawood_numbers(G, col_of_edge)
plus = sum(1 for v in h if h[v] == +1)
minus = sum(1 for v in h if h[v] == -1)
print(f"global h_φ: {plus} (+1) / {minus} (-1)")
# Verify both Kempe cycles through (0, 1) are constant.
K0 = trace_kempe(G, col_of_edge, (0, 1), (0, 1)) # red+blue
K1 = trace_kempe(G, col_of_edge, (0, 1), (0, 2)) # red+green
h_K0 = [h[v] for v in K0]
h_K1 = [h[v] for v in K1]
print(f"K_{{red, blue}} (len {len(K0)}): {K0}, h = {h_K0[0]} (const? {len(set(h_K0))==1})")
print(f"K_{{red, green}} (len {len(K1)}): {K1}, h = {h_K1[0]} (const? {len(set(h_K1))==1})")
print(f"V(K0) V(K1)| = {len(set(K0) | set(K1))} / {G.order()}")
# Canonical graph6
print(f"canonical graph6 = {G.canonical_label().graph6_string()}")
# Render PNG with planar layout
import matplotlib
matplotlib.use('Agg')
import matplotlib.pyplot as plt
pos = G.layout_planar()
fig, ax = plt.subplots(figsize=(10, 10), dpi=160)
ax.set_aspect('equal')
ax.axis('off')
for (u, v) in G.edge_iterator(labels=False):
c = COLOUR_NAME[col_of_edge[edge_key(u, v)]]
x1, y1 = pos[u]; x2, y2 = pos[v]
ax.plot([x1, x2], [y1, y2], color=c, linewidth=2.0, solid_capstyle='round')
K0set = set(K0); K1set = set(K1)
for v, (x, y) in pos.items():
if v in K0set and v in K1set:
face_c = '#bbbbff' # on both cycles
elif v in K0set or v in K1set:
face_c = '#ddddff'
else:
face_c = 'lightgrey'
ax.plot(x, y, 'o', markersize=18, markerfacecolor=face_c,
markeredgecolor='black', markeredgewidth=1.0)
ax.text(x, y, str(v), ha='center', va='center', fontsize=8)
xs = [p[0] for p in pos.values()]
ys = [p[1] for p in pos.values()]
pad = 0.5
ax.set_xlim(min(xs) - pad, max(xs) + pad)
ax.set_ylim(min(ys) - pad, max(ys) + pad)
os.makedirs(os.path.dirname(OUT_PNG), exist_ok=True)
fig.tight_layout()
fig.savefig(OUT_PNG, dpi=160, bbox_inches='tight')
plt.close(fig)
print(f"\nWrote: {OUT_PNG}")
if __name__ == '__main__':
main()