even_level: extend conjecture test to the cyclically-5-connected case (n=24)

Add the n=24 result to the Even Level Graph Generators paper: the dual of
the unique 44-vertex non-Hamiltonian cyclically-5-connected cubic planar
graph (Holton-McKay Fig. 2.10) -- a 24-vertex 5-connected triangulation,
the first conjecture test outside the 3-cut family -- is a bridge-derived
level graph, two verified bridge switches from an Even Level Graph
(source 19).

- Generate the graph rather than transcribe it: plantri -c5 lists all 6833
  5-connected 24-vertex triangulations; exactly one has a non-Hamiltonian
  dual, which also settles the uniqueness Holton-McKay left open at 44
  vertices (cyclically-5-connected triangulation <=> dual cubic graph).
- New abstract sentence + "cyclically-5-connected case: n=24" subsection,
  noting the classic 46-vertex Tutte graph is only cyclically 3-connected.
- Figure 6 (figures/fig210_dual.png): the dual T, parity-coloured, with the
  two introduced bridge edges {6,19} and {20,22} in green (style of Fig. 5).
- Experiments: test_fig210_dual_bridge.py (generate->filter->test pipeline),
  verify_fig210_witness.py (step-verifies the witness), draw_fig210_dual.py
  (figure), fig210_dual.g6 (the unique graph). paper.pdf rebuilt (10 pages).

Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
This commit is contained in:
2026-05-22 13:06:47 -04:00
parent 4693f63208
commit b45c3d5510
12 changed files with 657 additions and 59 deletions
@@ -0,0 +1,151 @@
"""Draw the dual of the unique 44-vertex non-Hamiltonian cyclically
5-connected cubic planar graph (Holton-McKay Fig. 2.10): a 24-vertex
5-connected triangulation T. Same style as draw_witnesses.py / Figure 5:
crossing-free planar drawing, vertices coloured by the fixed parity
labelling (blue even, orange odd), and the bridge edges introduced by the
two bridge switches from T's witness Even Level Graph drawn solid green.
Writes ../figures/fig210_dual.png.
"""
import sys
import os
sys.path.insert(0, '/Users/didericis/Code/math-research/papers/'
'level_resolutions_of_maximal_planar_graphs/experiments')
sys.path.insert(0, os.path.dirname(os.path.abspath(__file__)))
import networkx as nx
import matplotlib
matplotlib.use('Agg')
import matplotlib.pyplot as plt
from matplotlib.lines import Line2D
from sage.all import Graph # type: ignore
from tutte_dual_treecolor import dual_triangulation
from test_tutte_bridge import valid_parity_partitions_via_coloring
from test_fig210_dual_bridge import sage_to_nx
from fast_bridge import EdgeCode, parity_bridges
from test_conjecture import is_even_level_graph
HERE = os.path.dirname(os.path.abspath(__file__))
FDIR = os.path.join(HERE, '..', 'figures')
EVEN_C = '#9ecae1'
ODD_C = '#fdae6b'
def build():
g6 = open(os.path.join(HERE, 'fig210_dual.g6')).read().strip()
T, _ = dual_triangulation(sage_to_nx(Graph(g6)))
parts, _ = valid_parity_partitions_via_coloring(T)
labels = parts[9] # the witness-bearing partition
return T, labels
def neighbors(code, labels, state):
G = code.graph_of(state)
ok, emb = nx.check_planarity(G)
ea = {v: set() for v in code.nodes if labels[v] == 0}
oa = {v: set() for v in code.nodes if labels[v] == 1}
for u, v in G.edges():
if labels[u] == labels[v]:
(ea if labels[u] == 0 else oa)[u].add(v)
(ea if labels[u] == 0 else oa)[v].add(u)
br = parity_bridges(ea) | parity_bridges(oa)
for u, v in G.edges():
f1 = emb.traverse_face(u, v)
if len(f1) != 3:
continue
f2 = emb.traverse_face(v, u)
if len(f2) != 3:
continue
w = next(a for a in f1 if a not in (u, v))
x = next(b for b in f2 if b not in (u, v))
if w == x or G.has_edge(w, x) or labels[w] != labels[x]:
continue
if labels[u] == labels[v] and frozenset((u, v)) not in br:
continue
yield (state & ~(1 << code.bit(u, v))) | (1 << code.bit(w, x))
def elg_src(code, labels, state):
G = code.graph_of(state)
for s in code.nodes:
cs = labels[s]
nb = set(G.neighbors(s))
if not nb or any(labels[w] == cs for w in nb):
continue
ok, lv = is_even_level_graph(G, frozenset({s}))
if ok and all((lv[v] % 2 == 0) == (labels[v] == cs) for v in code.nodes):
return s
return None
def witness_added_edges(T, labels):
"""Backward bridge BFS to the ELG; return (source, [added bridge edges])."""
code = EdgeCode(T.nodes())
s0 = code.state_of(T)
parent = {s0: None}
frontier = [s0]
W = None
while frontier and W is None:
nf = []
for st in frontier:
if elg_src(code, labels, st) is not None:
W = st
break
for ns in neighbors(code, labels, st):
if ns not in parent:
parent[ns] = st
nf.append(ns)
if W:
break
frontier = nf
path = []
c = W
while c is not None:
path.append(c)
c = parent[c]
# path[0]=ELG ... path[-1]=T; edges added going ELG->T are present in T
added = []
for k in range(len(path) - 1):
A = set(map(frozenset, code.graph_of(path[k]).edges()))
B = set(map(frozenset, code.graph_of(path[k + 1]).edges()))
added.append(tuple(sorted(next(iter(B - A)))))
return elg_src(code, labels, W), added
def main():
os.makedirs(FDIR, exist_ok=True)
T, labels = build()
src, added = witness_added_edges(T, labels)
print('ELG source', src, 'bridge edges introduced', added)
fig, ax = plt.subplots(figsize=(7.5, 7.5))
pos = nx.planar_layout(T)
colors = [EVEN_C if labels[v] == 0 else ODD_C for v in T.nodes()]
hl = {frozenset(e) for e in added}
plain = [e for e in T.edges() if frozenset(e) not in hl]
nx.draw_networkx_edges(T, pos, edgelist=plain, ax=ax,
edge_color='#b0b0b0', width=0.9)
nx.draw_networkx_edges(T, pos, edgelist=[tuple(e) for e in hl], ax=ax,
edge_color='#2ca02c', width=2.6)
nx.draw_networkx_nodes(T, pos, node_color=colors, node_size=240,
edgecolors='#444444', linewidths=0.6, ax=ax)
nx.draw_networkx_labels(T, pos, font_size=8, ax=ax)
ax.margins(0.12)
ax.axis('off')
handles = [
Line2D([0], [0], marker='o', color='w', markerfacecolor=EVEN_C,
markeredgecolor='#444', markersize=9, label='even parity'),
Line2D([0], [0], marker='o', color='w', markerfacecolor=ODD_C,
markeredgecolor='#444', markersize=9, label='odd parity'),
Line2D([0], [0], color='#2ca02c', lw=2.6, label='bridge edge introduced'),
]
fig.legend(handles=handles, loc='lower center', ncol=3, fontsize=9,
frameon=False)
fig.tight_layout(rect=(0, 0.05, 1, 1))
out = os.path.join(FDIR, 'fig210_dual.png')
fig.savefig(out, dpi=160)
plt.close(fig)
print('wrote', out)
if __name__ == '__main__':
main()
@@ -0,0 +1 @@
ksP@@?PE?O?`@??_?O?A@?G??OG?O??G??A@??o??A???C@??E???@????O???E????G????OG???OG???G????B?????W????@?????A@????A@?????o?????G?????@@?????CC?????GG?????E??????@K
@@ -0,0 +1,95 @@
"""Bridge-derivability test for the dual of Holton-McKay's Fig. 2.10 graph
-- the smallest known non-Hamiltonian *cyclically 5-connected* cubic
planar graph (44 vertices, attributed to Tutte).
We obtain the graph by generation rather than transcription. A 44-vertex
cubic planar graph is the dual of a 24-vertex triangulation, and a cubic
graph is cyclically 5-connected iff its dual triangulation is 5-connected
(no separating 3- or 4-cycle). So we run
plantri -c5 -d -g 24
to list every 5-connected 24-vertex triangulation's cubic dual, keep the
non-Hamiltonian ones (Hamiltonicity of the dual = intertwining-tree of the
triangulation, by the paper's equivalence), and test each resulting
triangulation T = dual(H) for bridge-derivability. This is the conjecture's
first test in the cyclically-5-connected regime -- the family the n=21 and
46-vertex-Tutte duals (all only cyclically 3-connected) never reached.
Run after /tmp/nonham_duals.g6 has been produced by the Hamiltonicity
filter (lines: "<index> <graph6>").
"""
import sys
import os
import time
sys.path.insert(0, '/Users/didericis/Code/math-research/papers/'
'level_resolutions_of_maximal_planar_graphs/experiments')
sys.path.insert(0, os.path.dirname(os.path.abspath(__file__)))
import networkx as nx
from sage.all import Graph # type: ignore
from tutte_dual_treecolor import dual_triangulation
from fast_bridge import EdgeCode
from test_tutte_bridge import (
characterize, valid_parity_partitions_via_coloring, search_partition,
)
def sage_to_nx(G):
H = nx.Graph()
H.add_nodes_from(int(v) for v in G.vertices())
H.add_edges_from((int(u), int(v)) for u, v in G.edges(labels=False))
return H
def test_one(g6, cap=600_000, time_limit=180.0, log=print):
H = sage_to_nx(Graph(g6))
T, _ = dual_triangulation(H) # 24-vertex triangulation
info = characterize(T)
log('dual triangulation T: n=%(n)d m=%(m)d triangulation=%(is_triangulation)s '
'separating_triangles=%(separating_triangles)d four_connected=%(four_connected)s'
% info)
five_conn = (nx.node_connectivity(T) >= 5)
log(' vertex-connectivity(T) >= 5: %s [cyclically-5-connected cubic dual]'
% five_conn)
code = EdgeCode(T.nodes())
code.state0 = code.state_of(T)
n = info['n']
parts, n_col = valid_parity_partitions_via_coloring(T)
log(' %d valid parity partitions (from %d 4-colorings)' % (len(parts), n_col))
t0 = time.time()
for k, labels in enumerate(parts):
st, sz, depth = search_partition(code, labels, n, cap, time_limit)
if st == 'found':
log(' ==> BRIDGE-DERIVED: ELG witness at %d bridge switches '
'(partition %d, orbit>=%d, %.0fs)' % (depth, k, sz, time.time() - t0))
return 'bridge-derived', depth
if st in ('capped', 'timeout') or (k + 1) % 25 == 0:
log(' partition %d/%d: %s (orbit>=%d, %.0fs)'
% (k + 1, len(parts), st, sz, time.time() - t0))
# if every orbit fully exhausted with no witness -> conclusive NO
log(' ==> NO witness over all %d valid partitions (%.0fs)'
% (len(parts), time.time() - t0))
return 'no-witness', None
def main():
path = '/tmp/nonham_duals.g6'
rows = []
with open(path) as f:
for line in f:
line = line.strip()
if line:
idx, g6 = line.split(None, 1)
rows.append((int(idx), g6))
print('%d non-Hamiltonian cyclically-5-connected 44-vertex duals to test\n'
% len(rows), flush=True)
for idx, g6 in rows:
print('### candidate (plantri index %d): %s' % (idx, g6), flush=True)
verdict, depth = test_one(g6)
print('### verdict: %s\n' % verdict, flush=True)
if __name__ == '__main__':
main()
@@ -0,0 +1,79 @@
import sys
E='/Users/didericis/Code/math-research/papers/even_level_graph_generators/experiments'
L='/Users/didericis/Code/math-research/papers/level_resolutions_of_maximal_planar_graphs/experiments'
sys.path.insert(0,E); sys.path.insert(0,L)
import networkx as nx
from sage.all import Graph
from tutte_dual_treecolor import dual_triangulation
from test_tutte_bridge import valid_parity_partitions_via_coloring
from test_fig210_dual_bridge import sage_to_nx
from fast_bridge import EdgeCode, parity_bridges
from test_conjecture import is_even_level_graph
g6=open('/tmp/nonham_duals.g6').read().split(None,1)[1].strip()
H=sage_to_nx(Graph(g6)); T,_=dual_triangulation(H)
parts,_=valid_parity_partitions_via_coloring(T)
labels=parts[9]; code=EdgeCode(T.nodes()); s0=code.state_of(T); n=24
def neighbors(state):
G=code.graph_of(state); ok,emb=nx.check_planarity(G)
ea={v:set() for v in code.nodes if labels[v]==0}; oa={v:set() for v in code.nodes if labels[v]==1}
for u,v in G.edges():
if labels[u]==labels[v]: (ea if labels[u]==0 else oa)[u].add(v);(ea if labels[u]==0 else oa)[v].add(u)
br=parity_bridges(ea)|parity_bridges(oa); out=[]
for u,v in G.edges():
f1=emb.traverse_face(u,v)
if len(f1)!=3: continue
f2=emb.traverse_face(v,u)
if len(f2)!=3: continue
w=next(a for a in f1 if a not in(u,v)); x=next(b for b in f2 if b not in(u,v))
if w==x or G.has_edge(w,x) or labels[w]!=labels[x]: continue
if labels[u]==labels[v] and frozenset((u,v)) not in br: continue
out.append((state&~(1<<code.bit(u,v)))|(1<<code.bit(w,x)))
return out
def elg_src(state):
G=code.graph_of(state)
for s in code.nodes:
cs=labels[s]; nb=set(G.neighbors(s))
if not nb or any(labels[w]==cs for w in nb): continue
ok,lv=is_even_level_graph(G,frozenset({s}))
if ok and all((lv[v]%2==0)==(labels[v]==cs) for v in code.nodes): return s
return None
parent={s0:None}; frontier=[s0]; W=None
while frontier and W is None:
nf=[]
for st in frontier:
if elg_src(st) is not None: W=st; break
for ns in neighbors(st):
if ns not in parent: parent[ns]=st; nf.append(ns)
if W: break
frontier=nf
path=[]; c=W
while c is not None: path.append(c); c=parent[c]
# path[0]=ELG ... path[-1]=T (forward = ELG -> T)
src=elg_src(W)
print('=== Fig 2.10 dual T: bridge-derived, witness at %d bridge switches ==='%(len(path)-1))
print('ELG source s =',src)
ok,lv=is_even_level_graph(code.graph_of(W),frozenset({src}))
print('ELG verified (all level cycles even from s=%d): %s'%(src,ok))
print('max level =',max(lv.values()))
allgood=True
for k in range(len(path)-1):
A=code.graph_of(path[k]); B=code.graph_of(path[k+1])
EA=set(map(frozenset,A.edges())); EB=set(map(frozenset,B.edges()))
new=tuple(sorted(next(iter(EB-EA)))); rem=tuple(sorted(next(iter(EA-EB))))
# bridge condition on NEW edge in B's parity subgraph (forward result)
ea={v:set() for v in code.nodes if labels[v]==0}; oa={v:set() for v in code.nodes if labels[v]==1}
for u,v in B.edges():
if labels[u]==labels[v]: (ea if labels[u]==0 else oa)[u].add(v);(ea if labels[u]==0 else oa)[v].add(u)
br=parity_bridges(ea)|parity_bridges(oa)
if labels[new[0]]==labels[new[1]]:
valid=frozenset(new) in br; kind='same-parity bridge in %s subgraph'%('even' if labels[new[0]]==0 else 'odd')
else:
valid=True; kind='cross-parity (enters neither subgraph)'
allgood &= valid
print(' switch %d: remove level-edge %s, add %s [%s] valid=%s'%(k+1,rem,new,kind,valid))
print('ALL STEPS VALID BRIDGE SWITCHES:',allgood)
print('T is intertwining tree:', False, '(dual H non-Hamiltonian =', not Graph(g6).is_hamiltonian(),')')