even_level: extend to n=25 -- second internally-6-connected core, also bridge-derived

Enumerate non-Hamiltonian cyclically-5-connected cubic planar graphs by
running plantri -c5 -d for n in {23,25,26} (n=24 already in the previous
commit) and filtering for non-Hamiltonian dual:
  n=23  -> 0 of 1970   (recomputes Faulkner-Younger minimality)
  n=24  -> 1 of 6833   (the Tutte/Fig 2.10 graph)
  n=25  -> 1 of 23384  (new; unique 46-vertex one)
  n=26  -> 0 of 82625

Both T (n=24) and T_25 (n=25) verified internally 6-connected by exhaustive
5-cut scan: every 5-cut is the neighborhood of a degree-5 vertex. This is
the strongest connectivity a planar triangulation can have and the level
at which Birkhoff-style reductions terminate, so both are genuinely
irreducible bases of any decomposition argument.

T_25 is also bridge-derived: witness Even Level Graph from source 24
(max level 4) at depth 2, orbit only 3114 states. Forward switches:
remove {21,23} add {22,24}; remove {3,5} add {1,6}. Both adds are bridges
of the even parity subgraph. Same witness signature as T (minimum total
Betti, tiny orbit, depth 2).

New subsection "Beyond n=24: enumeration and the next 5-connected core",
abstract extended, new Figure 7 (core_n25_dual.png). Reproducibility
scripts: draw_core_witness.py and verify_core_witness.py (both
parametrized so they work on any 5-conn non-Ham-dual core's g6).

Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

papers/even_level_graph_generators/experiments/core_n25_dual.g6

@@ -0,0 +1 @@
+msP@@?PE?O?`@??_?O?A@?G??OG?O??G??A@??o??A???C@??C???A????_???C????o????_????_G???OC???E?????_????A?_???K?????K?????C?????@_G????B??????CC?????G??????GG?????CC?????@@??????BG

papers/even_level_graph_generators/experiments/draw_core_witness.py

@@ -0,0 +1,171 @@
+"""Draw a 5-connected non-Hamiltonian-dual core (= the dual of a non-Hamiltonian
+cyclically 5-connected cubic planar graph) as a parity-coloured planar graph
+with the bridge edges introduced by its witness Even Level Graph highlighted.
+Style matches Fig. 6 (the n=24 core).
+
+The script picks the first valid parity partition of minimal total Betti for
+which a backward bridge-orbit search returns an Even Level Graph, and prints
+the witness data (source, added bridge edges).
+
+Usage:
+  sage -python draw_core_witness.py <input_g6_file> <output_png_path>
+"""
+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
+
+EVEN_C = '#9ecae1'
+ODD_C = '#fdae6b'
+
+
+def betti(T, labels):
+    A = [v for v in T if labels[v] == 0]
+    B = [v for v in T if labels[v] == 1]
+    GA, GB = T.subgraph(A), T.subgraph(B)
+    return (GA.number_of_edges() - len(A) + nx.number_connected_components(GA)) + \
+           (GB.number_of_edges() - len(B) + nx.number_connected_components(GB))
+
+
+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 find_witness(T, labels, cap):
+    code = EdgeCode(T.nodes())
+    s0 = code.state_of(T)
+    parent = {s0: None}
+    frontier = [s0]
+    W = None
+    while frontier and W is None and len(parent) < cap:
+        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 len(parent) >= cap:
+                        break
+            if W or len(parent) >= cap:
+                break
+        if W:
+            break
+        frontier = nf
+    if W is None:
+        return None
+    path = []
+    c = W
+    while c is not None:
+        path.append(c)
+        c = parent[c]
+    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, len(path) - 1
+
+
+def main():
+    if len(sys.argv) < 3:
+        print('usage: draw_core_witness.py <input_g6_file> <output_png_path>')
+        sys.exit(1)
+    in_g6_path, out_png = sys.argv[1], sys.argv[2]
+    g6 = open(in_g6_path).read().strip()
+    T, _ = dual_triangulation(sage_to_nx(Graph(g6)))
+    parts, _ = valid_parity_partitions_via_coloring(T)
+    order = sorted(range(len(parts)), key=lambda k: betti(T, parts[k]))
+    chosen = None
+    for k in order[:200]:
+        r = find_witness(T, parts[k], cap=40000)
+        if r is not None:
+            chosen = (k, parts[k], r)
+            break
+    if chosen is None:
+        print('no witness found in scanned partitions; aborting')
+        sys.exit(2)
+    k, labels, (src, added, depth) = chosen
+    print('partition=%d  source=%d  depth=%d  added=%s' % (k, src, depth, added))
+
+    fig, ax = plt.subplots(figsize=(8, 8))
+    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))
+    os.makedirs(os.path.dirname(out_png), exist_ok=True)
+    fig.savefig(out_png, dpi=160)
+    plt.close(fig)
+    print('wrote', out_png)
+
+
+if __name__ == '__main__':
+    main()

papers/even_level_graph_generators/experiments/verify_core_witness.py

@@ -0,0 +1,101 @@
+"""Step-verify the bridge-derivability witness for a 5-connected
+non-Hamiltonian-dual core. Same outputs as verify_fig210_witness.py
+(parity partition, ELG source/max level, both removed and added edges per
+forward switch, bridge-condition validity check) but parametrized so it
+works on any core's graph6.
+
+Usage:
+  sage -python verify_core_witness.py <input_g6_file>
+"""
+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
+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
+from draw_core_witness import betti, neighbors, elg_src, find_witness
+
+
+def main():
+    if len(sys.argv) < 2:
+        print('usage: verify_core_witness.py <input_g6_file>')
+        sys.exit(1)
+    g6 = open(sys.argv[1]).read().strip()
+    T, _ = dual_triangulation(sage_to_nx(Graph(g6)))
+    parts, _ = valid_parity_partitions_via_coloring(T)
+    order = sorted(range(len(parts)), key=lambda k: betti(T, parts[k]))
+
+    chosen = None
+    for k in order[:200]:
+        r = find_witness(T, parts[k], cap=40000)
+        if r is not None:
+            chosen = (k, parts[k], r)
+            break
+    assert chosen is not None, 'no witness found'
+    k, labels, (src, _, _) = chosen
+
+    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]
+
+    ok, lv = is_even_level_graph(code.graph_of(W), frozenset({src}))
+    print('partition %d, source %d, max level %d, depth %d, ELG verified %s'
+          % (k, src, max(lv.values()), len(path) - 1, ok))
+    print('parity even =', sorted(v for v in T if labels[v] == 0))
+    print('parity odd  =', sorted(v for v in T if labels[v] == 1))
+
+    all_valid = True
+    for i in range(len(path) - 1):
+        A = set(map(frozenset, code.graph_of(path[i]).edges()))
+        B = set(map(frozenset, code.graph_of(path[i + 1]).edges()))
+        new = tuple(sorted(next(iter(B - A))))
+        rem = tuple(sorted(next(iter(A - B))))
+        Gp = code.graph_of(path[i + 1])
+        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 Gp.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)'
+        all_valid &= valid
+        print('  switch %d: remove %s, add %s  [%s]  valid=%s'
+              % (i + 1, rem, new, kind, valid))
+    print('ALL STEPS VALID BRIDGE SWITCHES:', all_valid)
+
+
+if __name__ == '__main__':
+    main()